#440 (Oct 10, 2017, 12:50:11 AM)

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

Started by an SCM change

This run spent:

• 9.3 sec waiting;
• 1 hr 36 min build duration;
• 1 hr 37 min total from scheduled to completion.