Changes

Summary

merge
removed axiomatization, integrated distinct-degree-factorization as optional
tuned docu
manual merge
integrated distinct degree factorization into finite field factorization algorithm

Changeset 7266:c00faa7bddac by rene thiemann _rene.thiemann@uibk.ac.at_: merge
Changeset 7265:0bd09f201588 by rene thiemann _rene.thiemann@uibk.ac.at_: removed axiomatization, integrated distinct-degree-factorization as optional
The file was modified	`thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
Changeset 7264:260ab3b964ea by rene thiemann _rene.thiemann@uibk.ac.at_: tuned docu
The file was modified	`thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization.thy` (diff)
Changeset 7263:e9b9e68f0c4d by rene thiemann _rene.thiemann@uibk.ac.at_: manual merge
Changeset 7262:74b32cf8816d by rene thiemann _rene.thiemann@uibk.ac.at_: integrated distinct degree factorization into finite field factorization algorithm
The file was added	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization.thy`
The file was added	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy`
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/Berlekamp_Zassenhaus.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was removed	`thys/Berlekamp_Zassenhaus/Berlekamp_Record_Based.thy`