#1146 (Oct 9, 2017, 10:02:10 PM)

1. tuned proof (detail / hgweb)
2. euclidean rings need no normalization (detail / hgweb)
3. prefer official global interface to remove code equations, leaving problematic situation due to bypassing of native code declarations as it is (detail / hgweb)
4. elementary definition of division on natural numbers (detail / hgweb)
5. removed unused lemmas (detail / hgweb)
6. tuned proofs (detail / hgweb)
7. avoid name clashes on interpretation of abstract locales (detail / hgweb)
8. abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel (detail / hgweb)
9. Polynomial_Factorial does not depend on Field_as_Ring as such (detail / hgweb)
10. avoid unnecessary qualification (detail / hgweb)

Started by an SCM change

This run spent:

• 8.8 sec waiting;
• 4 hr 32 min build duration;
• 4 hr 32 min total from scheduled to completion.