Changes

Summary

Second batch of AFP adjustments to new Factorial Rings
Merged
Merged
Adapted AFP to changes in Euclidean rings etc.

Changeset 6949:4206268ad833 by eberlm _eberlm@in.tum.de_: Second batch of AFP adjustments to new Factorial Rings
The file was modified	`thys/CAVA_Automata/Automata_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/Digraph_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_LTL_Conv.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Default.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_LC.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Set_Default.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Set_LC.thy` (diff)
The file was modified	`thys/FileRefinement/FileRefinement.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_GBG_Code.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_SCC_Code.thy` (diff)
The file was modified	`thys/Promela/Promela.thy` (diff)
The file was modified	`thys/Promela/PromelaDatastructures.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)
Changeset 6948:73feab994e58 by eberlm _eberlm@in.tum.de_: Merged
Changeset 6947:6e590d384ce3 by eberlm _eberlm@in.tum.de_: Merged
Changeset 6946:3bb1425f7ca9 by eberlm _eberlm@in.tum.de_: Adapted AFP to changes in Euclidean rings etc.
The file was modified	`thys/Algebraic_Numbers/Algebraic_Number_Tests.thy` (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/Complex_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Factorization.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Unique_Factorization_Poly.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant_Impl.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Kronecker_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Division.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/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_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)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)