Changes

Summary

dedicated definition for coprimality
prefer abbreviation coprime

Changeset 8541:d070575681b0 by haftmann: dedicated definition for coprimality
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Method.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Eval_Numeral.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem_Examples.thy` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi.ML` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Hensel.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Rat_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Gcd_Finite_Field_Impl.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Reconstruction.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Monadic_Language.thy` (diff)
The file was modified	`thys/Count_Complex_Roots/Extended_Sturm.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Arithmetic_Summatory_Asymptotics.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Misc.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Product.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Euler_Products.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Multiplicative_Function.thy` (diff)
The file was modified	`thys/Elliptic_Curves_Group_Law/Elliptic_Test.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat3.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat4.thy` (diff)
The file was modified	`thys/Fermat3_4/Quad_Form.thy` (diff)
The file was modified	`thys/Impossible_Geometry/Impossible_Geometry.thy` (diff)
The file was modified	`thys/Koenigsberg_Friendship/FriendshipTheory.thy` (diff)
The file was modified	`thys/Lehmer/Lehmer.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Factorizations.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Misc.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Test.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy` (diff)
The file was modified	`thys/Linear_Recurrences/RatFPS.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Rational_FPS_Solver.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Perfect.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/PerfectBasics.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Sigma.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Roots_Unity.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_Polynomial_Factorial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Unsorted.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Stern_Brocot/Stern_Brocot_Tree.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Tarski/PolyMisc.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/Subresultants/Dichotomous_Lazard.thy` (diff)
The file was modified	`thys/SumSquares/TwoSquares.thy` (diff)
The file was modified	`thys/WorkerWrapper/Streams.thy` (diff)
Changeset 8540:af23e0a6fd58 by haftmann: prefer abbreviation coprime
The file was modified	`thys/Fermat3_4/Fermat3.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat4.thy` (diff)
The file was modified	`thys/Fermat3_4/Quad_Form.thy` (diff)
The file was modified	`thys/Fermat3_4/document/root.tex` (diff)