Changes

Summary

1. merged
2. tuned ML --- clarified use of context; tuned message;
3. tuned --- fewer clones;
4. updated to jEdit plugin Highlight 2.5;
5. proper tactic combinator;
6. proper file headers;
7. clarified context; clarified modules;
8. more accurate treatment of context;
9. updated email address
10. removed some 'private' modifiers from HOL-Computational_Algebra
11. merged
12. merged
13. more robust Variable.revert_bounds (see also b12f2cef3ee5);
14. more accurate treatment of context;
15. tuned -- proper names/scopes for contexts;
16. clarified context;
17. clarified context;
18. tuned;
19. unused;
20. more accurate treatment of context; declare generated bounds for the sake of recdef, which has variables leaking from local context;
21. isabelle regenerate_cooper;
22. revert bbfed17243af, breaks HOL-Proofs extraction;
23. tuned;
24. tuned;
25. proper p' instead of p (amending 52c7c42e7e27);
26. proper context for Goal.prove_internal;
27. discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; Simplifier and equational conversions demand a proper proof context;
28. more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
29. tuned;
30. tuned;
31. tuned;
32. spelling;
33. clarified context;
34. clarified signature;
35. tuned Vampire configuration to use TFX in Sledgehammer
36. added Mirabelle action presburger
37. added timing to Mirabelle action arith
38. added error message on invalid Mirabelle action