#1075 (Dec 4, 2019, 12:50:10 AM)

1. merged (detail / hgweb)
2. clarified export of consts: recursion is accessible via spec_rules; (detail / hgweb)
3. more operations; (detail / hgweb)
4. Removed orphaned theory from HOL-Analysis (detail / hgweb)
5. merged (detail / hgweb)
6. clarified position for spec rule: like entity; (detail / hgweb)
7. clarified name: avoid clashes; (detail / hgweb)
8. proper dynamic position of application context, e.g. relevant for 'global_interpretation'; (detail / hgweb)
9. proper treatment of variable names; (detail / hgweb)
10. proper spec_rule name via naming/binding/Morphism.binding; (detail / hgweb)
11. more informative spec rules; (detail / hgweb)
12. more robust; (detail / hgweb)
13. more informative export; (detail / hgweb)
14. tuned signature -- following Export_Theory.Spec_Rule in Scala; (detail / hgweb)
15. tuned comment; (detail / hgweb)
16. clarified export of spec rules: more like locale; (detail / hgweb)
17. formal position for spec rule (not significant for equality); (detail / hgweb)
18. proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory"; (detail / hgweb)
19. proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory"; (detail / hgweb)
20. tuned -- avoid confusion of fun_t with fun_lhs; (detail / hgweb)
21. avoid shadowing of local bindings -- more maintainable; (detail / hgweb)
22. export spec rules; (detail / hgweb)
23. Reorganised HOL-Complex_Analysis (detail / hgweb)
24. split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological (detail / hgweb)

Started by an SCM change

This run spent:

• 8.3 sec waiting;
• 1 hr 10 min build duration;
• 1 hr 10 min total from scheduled to completion.