Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merge
  2. prefer gcd_rat_poly over gcd (10x faster)
  3. code-unfold lemma for gcd_rat_poly
  4. added gcd_rat_poly which works via gcd_int_poly
  5. improved code equation
Changeset 6227:63c395e3713e by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 6226:c96c77bcab21 by rene thiemann _rene.thiemann@uibk.ac.at_:
prefer gcd_rat_poly over gcd (10x faster)
The file was modified thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Roots.thy (diff)
The file was modified thys/Algebraic_Numbers/Sturm_Rat.thy (diff)
The file was modified thys/Polynomial_Factorization/Berlekamp_Hensel_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
Changeset 6225:b817d3d521b6 by rene thiemann _rene.thiemann@uibk.ac.at_:
code-unfold lemma for gcd_rat_poly
The file was modified thys/Polynomial_Factorization/Polynomial_Division.thy (diff)
Changeset 6224:233ffb03469d by rene thiemann _rene.thiemann@uibk.ac.at_:
added gcd_rat_poly which works via gcd_int_poly
The file was modified thys/Polynomial_Factorization/Gauss_Lemma.thy (diff)
The file was modified thys/Polynomial_Factorization/Polynomial_Division.thy (diff)
Changeset 6223:3964733797ff by rene thiemann _rene.thiemann@uibk.ac.at_:
improved code equation
The file was modified thys/Polynomial_Factorization/Gauss_Lemma.thy (diff)