#1207 (Oct 9, 2017, 7:18:49 PM)

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

Started by an SCM change

This run spent:

• 5 min 2 sec waiting;
• 6 hr 9 min build duration;
• 6 hr 14 min total from scheduled to completion.