Changes

Summary

adjusted to refined Euclidean_Algorithm.thy in distribution
changed fact

Changeset 7533:c38d81f1fd06 by haftmann: adjusted to refined Euclidean_Algorithm.thy in distribution
The file was modified	`thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.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/Code_Abort_Gcd.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field.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/Polynomial_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Resultant.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Inverse_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Hermite/Hermite.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)
Changeset 7532:48d2e2c76ca9 by haftmann: changed fact
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)