Changes

Summary

merge
activated 32-bit factorization engine (thanks to Andreas for pointing to "Native_Word/Code_Target_Bits_Int")
prepared 32-bit support for hensel-lifting and prime-selection
docu
improved code equation for "x >> 1"
completed 32-bit implementation of GF(p), problems with export-code
towards soundness of 32-bit number implementation of GF(p)
definition of 32-bit implementation
minor restructuring
cleanup
more flexible implementation for GF(p)
towards more generic implementation interface of finite field factorization

Changeset 7321:be10c54da15f by rene thiemann _rene.thiemann@uibk.ac.at_: merge
Changeset 7320:c6b6451f4032 by rene thiemann _rene.thiemann@uibk.ac.at_: activated 32-bit factorization engine (thanks to Andreas for pointing to "Native_Word/Code_Target_Bits_Int")
The file was modified	`thys/Algebraic_Numbers/ROOT` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/ROOT` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
Changeset 7319:54d088e97e14 by rene thiemann _rene.thiemann@uibk.ac.at_: prepared 32-bit support for hensel-lifting and prime-selection
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
Changeset 7318:52163d4e9135 by rene thiemann _rene.thiemann@uibk.ac.at_: docu
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
Changeset 7317:415bff98d2cc by rene thiemann _rene.thiemann@uibk.ac.at_: improved code equation for "x >> 1"
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
Changeset 7316:e696bb855fa6 by rene thiemann _rene.thiemann@uibk.ac.at_: completed 32-bit implementation of GF(p), problems with export-code
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field_Record_Based.thy` (diff)
Changeset 7315:5cbe096c364b by rene thiemann _rene.thiemann@uibk.ac.at_: towards soundness of 32-bit number implementation of GF(p)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
Changeset 7314:3d29908bf699 by rene thiemann _rene.thiemann@uibk.ac.at_: definition of 32-bit implementation
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
Changeset 7313:eb4176121f93 by rene thiemann _rene.thiemann@uibk.ac.at_: minor restructuring
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
Changeset 7312:8bc6b6f2232d by rene thiemann _rene.thiemann@uibk.ac.at_: cleanup
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
Changeset 7311:c449bc243801 by rene thiemann _rene.thiemann@uibk.ac.at_: more flexible implementation for GF(p)
The file was modified	`thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Polynomial_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
Changeset 7310:4e9c4ca7dc27 by rene thiemann _rene.thiemann@uibk.ac.at_: towards more generic implementation interface of finite field factorization
The file was modified	`thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Polynomial_Record_Based.thy` (diff)