#1362 (Dec 17, 2020, 12:50:10 AM)

1. merged (detail / hgweb)
2. proper support for Windows/Cygwin; (detail / hgweb)
3. updated to zipperposition-2.0 and ocaml-4.07, which is required for it; (detail / hgweb)
4. more checks; (detail / hgweb)
5. merged (detail / hgweb)
6. simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1) (detail / hgweb)
7. added missing +1 to T_insert (for function call) (detail / hgweb)
8. merged (detail / hgweb)
9. afford more reactive input; (detail / hgweb)
10. more NEWS; (detail / hgweb)
11. more documentation; (detail / hgweb)
12. added action isabelle.goto-entity to follow links in a narrow formal sense; (detail / hgweb)
13. tuned signature; (detail / hgweb)
14. clarified select_entity (again): it is meant as approximation to "refactoring" and thus only makes sense for defs within the same buffer; (detail / hgweb)
15. clarified caret focus modifier, depending on option "jedit_focus_modifier"; (detail / hgweb)
16. tuned; (detail / hgweb)
17. tuned; (detail / hgweb)
18. enabled FOOL for E (detail / hgweb)
19. merged (detail / hgweb)
20. tuned name generation in tptp to not depend on shadowing (detail / hgweb)
21. tuned lambda translation for fool (detail / hgweb)
22. generate unique variable names in tptp (detail / hgweb)
23. proper handling of true and false in tptp (detail / hgweb)
24. proper eta-expansion to avoid lambdas in tptp fool (detail / hgweb)
25. proper proxification for fool + refactoring (detail / hgweb)
26. proper renaming of THF_Lambda_Bool_Free (detail / hgweb)
27. proper parsing of type encoding;
    tuned naming (detail / hgweb)
28. proper handling of builtins in TFX (detail / hgweb)
29. proper generation of TPTP output for higher order builtins (detail / hgweb)
30. tuned (detail / hgweb)

Started by an SCM change

This run spent:

• 9.5 sec waiting;
• 1 hr 29 min build duration;
• 1 hr 29 min total from scheduled to completion.