#1554 (Sep 22, 2021, 1:37:56 AM)

1. clarified antiquotations; (detail / hgweb)
2. clarified antiquotations; (detail / hgweb)
3. clarified antiquotations; (detail / hgweb)
4. clarified partial application: immediate check of object-logic, and avoidance of context within closure; (detail / hgweb)
5. merged (detail / hgweb)
6. clarified antiquotations; (detail / hgweb)
7. ML antiquotations for object-logic judgment; (detail / hgweb)
8. proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep; (detail / hgweb)
9. clarified modules; (detail / hgweb)
10. clarified modules; (detail / hgweb)
11. more uniform syntax; (detail / hgweb)
12. permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone; (detail / hgweb)
13. NEWS; (detail / hgweb)
14. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; (detail / hgweb)
15. localized command 'syntax' and 'no_syntax'; (detail / hgweb)
16. tuned; (detail / hgweb)
17. clarified signature; (detail / hgweb)
18. clarified signature; (detail / hgweb)

Started by an SCM change

This run spent:

• 47 min waiting;
• 2 hr 6 min build duration;
• 2 hr 54 min total from scheduled to completion.