#731 (Sep 10, 2018, 12:50:09 AM)

1. Removed problematic rules from continuous_intros (detail / hgweb)
2. merged (detail / hgweb)
3. tuned (detail / hgweb)
4. tuned message (again); (detail / hgweb)
5. proper binding positions within the defining command transaction; (detail / hgweb)
6. smash position to avoid position of other file "~~/src/HOL/BNF_Composition.thy" (due to "bnf ID"), e.g. relevant for "HOL-Nominal-Examples.Class1"; (detail / hgweb)
7. clarified message; (detail / hgweb)
8. tuned message; (detail / hgweb)
9. clarified theory progress; (detail / hgweb)

Started by an SCM change

This run spent:

• 7.5 sec waiting;
• 1 hr 14 min build duration;
• 1 hr 14 min total from scheduled to completion.