#1417 (Feb 23, 2018, 5:30:41 PM)

1. merged (detail / hgweb)
2. merged (detail / hgweb)
3. tuned proofs -- more explicit use of facts from 'interpret'; (detail / hgweb)
4. replaced vacuous class nat_int/real_int by more elementary locale + interpretation: this avoids implicit sort constraints imposed on theorems, as well as pointless dictionary constructions (foo_dict); (detail / hgweb)
5. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

• 8.1 sec waiting;
• 3 hr 24 min build duration;
• 3 hr 24 min total from scheduled to completion.