Diffusion afp-devel 0f0adba767a3

adapted to isabelle-dev/e0237f2eb49d
0f0adba767a3
Actions

Tags

None

Subscribers

None

Description

adapted to isabelle-dev/e0237f2eb49d

Details

Provenance

Authored on

Parents

rAFP8b6582b73697: merged

Branches

Unknown

Tags

Unknown

Event Timeline

pruvisto committed rAFP0f0adba767a3: adapted to isabelle-dev/e0237f2eb49d.Jan 21 2020, 11:55 PM

Changes (38)

Path

Size

thys/

Algebraic_Numbers/

Algebraic_Numbers_Prelim.thy

Berlekamp_Zassenhaus/

Arithmetic_Record_Based.thy

Berlekamp_Type_Based.thy

Chinese_Remainder_Poly.thy

Code_Abort_Gcd.thy

Factorize_Int_Poly.thy

Factorize_Rat_Poly.thy

Finite_Field.thy

Hensel_Lifting.thy

Square_Free_Factorization_Int.thy

Unique_Factorization.thy

Unique_Factorization_Poly.thy

Budan_Fourier/

Count_Complex_Roots/

More_Polynomials.thy

Hermite/

Jordan_Normal_Form/

Determinant_Impl.thy

LLL_Basis_Reduction/

Missing_Lemmas.thy

Linear_Recurrences/

Factorizations.thy

Linear_Homogenous_Recurrences.thy

Linear_Inhomogenous_Recurrences.thy

Linear_Recurrences_Misc.thy

Partial_Fraction_Decomposition.thy

Rational_FPS_Asymptotics.thy

Rational_FPS_Solver.thy

Solver/

Show_RatFPS.thy

Mason_Stothers/

Mason_Stothers.thy

Polynomial_Factorization/

Missing_Polynomial_Factorial.thy

Prime_Factorization.thy

Square_Free_Factorization.thy

Polynomial_Interpolation/

Missing_Polynomial.thy

Missing_Unsorted.thy

Ring_Hom_Poly.thy

Probabilistic_Prime_Tests/

Algebraic_Auxiliaries.thy

Sturm_Sequences/

Lib/

Misc_Polynomial.thy

Sturm_Tarski/

Subresultants/

Subresultant_Gcd.thy

rAFP0f0adba767a3

thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy

Loading...

thys/Algebraic_Numbers/Sturm_Rat.thy

Loading...

thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy

Loading...

thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy

Loading...

thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy

Loading...

thys/Berlekamp_Zassenhaus/Code_Abort_Gcd.thy

Loading...

thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy

Loading...

thys/Berlekamp_Zassenhaus/Factorize_Rat_Poly.thy

Loading...

thys/Berlekamp_Zassenhaus/Finite_Field.thy

Loading...

thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy

Loading...

thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy

Loading...

thys/Berlekamp_Zassenhaus/Unique_Factorization.thy

Loading...

thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy

Loading...

thys/Budan_Fourier/BF_Misc.thy

Loading...

thys/Count_Complex_Roots/More_Polynomials.thy

Loading...

thys/Hermite/Hermite.thy

Loading...

thys/Jordan_Normal_Form/Determinant_Impl.thy

Loading...

thys/LLL_Basis_Reduction/Missing_Lemmas.thy

Loading...

thys/Linear_Recurrences/Factorizations.thy

Loading...

thys/Linear_Recurrences/Linear_Homogenous_Recurrences.thy

Loading...

thys/Linear_Recurrences/Linear_Inhomogenous_Recurrences.thy

Loading...

thys/Linear_Recurrences/Linear_Recurrences_Misc.thy

Loading...

thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy

Loading...

thys/Linear_Recurrences/RatFPS.thy

Loading...

thys/Linear_Recurrences/Rational_FPS_Asymptotics.thy

Loading...

thys/Linear_Recurrences/Rational_FPS_Solver.thy

Loading...

thys/Linear_Recurrences/Solver/Show_RatFPS.thy

Loading...

thys/Mason_Stothers/Mason_Stothers.thy

Loading...

thys/Polynomial_Factorization/Missing_Polynomial_Factorial.thy

Loading...

thys/Polynomial_Factorization/Prime_Factorization.thy

Loading...

thys/Polynomial_Factorization/Square_Free_Factorization.thy

Loading...

thys/Polynomial_Interpolation/Missing_Polynomial.thy

Loading...

thys/Polynomial_Interpolation/Missing_Unsorted.thy

Loading...

thys/Polynomial_Interpolation/Ring_Hom_Poly.thy

Loading...

thys/Probabilistic_Prime_Tests/Algebraic_Auxiliaries.thy

Loading...

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

Loading...

thys/Sturm_Tarski/PolyMisc.thy

Loading...

thys/Subresultants/Subresultant_Gcd.thy

Loading...