Changes

Summary

1. merged
2. tuned: less oo-non-sense;
3. operations for graph display;
4. tuned signature;
5. dependencies of entries vs. sessions; json output like "isabelle afp_dependencies"; misc tuning;
6. some administrative support for AFP;
7. tuned;
8. clarified signature: public access to ROOT file syntax;
9. euclidean rings need no normalization
10. more fundamental definition of div and mod on int
11. one uniform type class for parity structures
12. generalized some rules
13. avoid variant of mk_sum
14. adjusted implementation according to comment
15. dropped duplicates
16. generalized simproc
17. replaced recdef were easy to replace
18. elementary definition of division on natural numbers
19. tuned structure
20. abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
21. Polynomial_Factorial does not depend on Field_as_Ring as such
22. avoid name clashes on interpretation of abstract locales
23. avoid trivial definition
24. canonical introduction and destruction rules for pairwise
25. avoid fact name clashes
26. spelling and tuned whitespace
27. tuned
28. fundamental property of division by units
29. removed mere toy example from library
30. tuned proofs
31. dropped dead code
32. Fixed the theorem name "closed_imp_fip_compact"
33. new material about connectedness, etc.