Summary
- euclidean rings need no normalization
- more fundamental definition of div and mod on int
- one uniform type class for parity structures
- generalized some rules
- avoid variant of mk_sum
- adjusted implementation according to comment
- dropped duplicates
- generalized simproc
- replaced recdef were easy to replace
- elementary definition of division on natural numbers
- tuned structure
- abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
- Polynomial_Factorial does not depend on Field_as_Ring as such
- avoid name clashes on interpretation of abstract locales
- avoid trivial definition
- canonical introduction and destruction rules for pairwise
- avoid fact name clashes
- spelling and tuned whitespace
- tuned
- fundamental property of division by units
- removed mere toy example from library
- tuned proofs
- dropped dead code
- Fixed the theorem name "closed_imp_fip_compact"