Changes

Summary

session containing computational algebra
more approproiate placement of theories MiscAlgebra and Multiplicate_Group

Changeset 7773:e30011852263 by haftmann: session containing computational algebra
The file was modified	`thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Code_Abort_Gcd.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Bernoulli/Bernoulli_FPS.thy` (diff)
The file was modified	`thys/Catalan_Numbers/Catalan_Numbers.thy` (diff)
The file was modified	`thys/Catalan_Numbers/ROOT` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/ROOT` (diff)
The file was modified	`thys/Coinductive/Examples/Hamming_Stream.thy` (diff)
The file was modified	`thys/Coinductive/ROOT` (diff)
The file was modified	`thys/Deep_Learning/PP_MPoly.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_Univariate.thy` (diff)
The file was modified	`thys/Deep_Learning/ROOT` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/E_Transcendental/E_Transcendental.thy` (diff)
The file was modified	`thys/E_Transcendental/ROOT` (diff)
The file was modified	`thys/Echelon_Form/Code_Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat4.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Fraction_Field.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/ROOT` (diff)
The file was modified	`thys/Knot_Theory/Kauffman_Matrix.thy` (diff)
The file was modified	`thys/Knot_Theory/ROOT` (diff)
The file was modified	`thys/Koenigsberg_Friendship/ROOT` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers_Misc.thy` (diff)
The file was modified	`thys/Liouville_Numbers/ROOT` (diff)
The file was modified	`thys/Perfect-Number-Thm/PerfectBasics.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Fundamental_Theorem_Algebra_Factorized.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/ROOT` (diff)
The file was modified	`thys/Polynomial_Interpolation/Improved_Code_Equations.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Neville_Aitken_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/ROOT` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was modified	`thys/RSAPSS/Pdifference.thy` (diff)
The file was modified	`thys/RSAPSS/ROOT` (diff)
The file was modified	`thys/RSAPSS/Wordarith.thy` (diff)
The file was modified	`thys/Real_Impl/ROOT` (diff)
The file was modified	`thys/Real_Impl/Real_Impl_Auxiliary.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/ROOT` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Show/Show_Poly.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Sturm_Tarski/PolyMisc.thy` (diff)
The file was modified	`thys/Sturm_Tarski/ROOT` (diff)
Changeset 7772:e01fc8ecb411 by haftmann: more approproiate placement of theories MiscAlgebra and Multiplicate_Group
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy` (diff)
The file was modified	`thys/E_Transcendental/E_Transcendental.thy` (diff)
The file was modified	`thys/Koenigsberg_Friendship/ROOT` (diff)
The file was modified	`thys/Lehmer/Lehmer.thy` (diff)
The file was modified	`thys/Lehmer/ROOT` (diff)
The file was removed	`thys/Lehmer/Multiplicative_Group.thy`