Changes

Summary

1. euclidean rings need no normalization
2. more fundamental definition of div and mod on int
3. one uniform type class for parity structures
4. generalized some rules
5. avoid variant of mk_sum
6. adjusted implementation according to comment
7. dropped duplicates
8. generalized simproc
9. replaced recdef were easy to replace
10. elementary definition of division on natural numbers
11. tuned structure
12. abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
13. Polynomial_Factorial does not depend on Field_as_Ring as such
14. avoid name clashes on interpretation of abstract locales
15. avoid trivial definition
16. canonical introduction and destruction rules for pairwise
17. avoid fact name clashes
18. spelling and tuned whitespace
19. tuned
20. fundamental property of division by units
21. removed mere toy example from library
22. tuned proofs
23. dropped dead code
24. Fixed the theorem name "closed_imp_fip_compact"