#1585 (Oct 30, 2021, 12:50:06 AM)

1. clarified antiquotations; (detail / hgweb)
2. more robust subgoal addressing; (detail / hgweb)
3. proper subgoal addressing; (detail / hgweb)
4. clarified antiquotations; (detail / hgweb)
5. recursive find_eq, not find_dist; (detail / hgweb)
6. misc tuning and clarification; (detail / hgweb)
7. clarified antiquotations; (detail / hgweb)
8. order_tac: prevent potential bug, improve perf and tracing
   
   - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p. (detail / hgweb)
9. misc tuning and clarification; (detail / hgweb)
10. clarified antiquotations; (detail / hgweb)
11. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; (detail / hgweb)
12. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; (detail / hgweb)
13. avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); (detail / hgweb)
14. added Thm.instantiate_beta;
    tuned; (detail / hgweb)
15. moved generic implementation into HOL-Main (detail / hgweb)

Started by an SCM change

This run spent:

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