Changes

Summary

1. get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options
2. merged
3. NEWS;
4. proper example;
5. more tests;
6. more robust: component might be absent;
7. clarified global state: allow to deactivate main plugin;
8. more robust (again): allow to deactivate main plugin;
9. tuned signature;
10. more complete dockables;
11. more robust (see 4d91b6d5d49c);
12. clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
13. more robust;
14. tuned;
15. avoid non-standard encoding;
16. proper cross-platform build: jdk component is required for ISABELLE_SETUP_CLASSPATH in other_isabelle;
17. more robust classpath: skip empty entries;
18. more robust: avoid duplicate classpath entries;
19. build.props for isabelle.jar, including isabelle.jedit; build minimal Isabelle/jEdit plugins on the spot; regular "jedit" component: discontinued special "jedit_build"; Isabelle/Scala services via jars, instead of settings;
20. more robust;
21. more portable: avoid Windows CRLF in classpath output;
22. proper lines (amending 59b6f0462086);
23. more systematic treatment of encodings;
24. tuned;
25. extended the 'corec' format slightly
26. prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent
27. tuning
28. rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
29. correctly translate constructor argument in 'primrec'
30. simplified a few proofs
31. revisited ac28714b7478: more faithful preplaying with chained facts
32. wait for E 2.7 before using 'ite' in HO mode
33. added alternative E binary name
34. parse logical operators in the right order w.r.t. backtracking
35. improved warning
36. adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
37. operations for symbolic computation of bit operations
38. proper local context
39. shasum for project meta-info;
40. even more strict shasum (amending c9771e1b3223);
41. clarified Isabelle meta-info within jar;
42. strict shasum: this is used on input files;
43. clarified modules; clarified messages; clarified return code;
44. support for command-line operations;
45. operations for all components;
46. clarified signature;
47. merged
48. rebuild component;
49. expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
50. support expand_platform_path, which is reminiscent of isabelle.Path.expand;
51. skip scalac for Java build;
52. support mixed Scala/Java build; clarified scalac/javac options;
53. clarified javac options;
54. clarified syntax: similar to URL;
55. clarified signature;
56. more robust;
57. more robust;
58. more compiler_deps via "requirements", notably jar list from settings; proper Files.createDirectories;
59. clarified component settings;
60. clarified shasum: sources / resources within jar;
61. tuned signature;
62. clarified modules;
63. merged
64. fixed HOL-TPTP following f58108b7a60c
65. documented Sledgehammer option "induction_rules"
66. refactored Sledgehammer option "induction_rules"
67. promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
68. jenkins: add pre/post-hook results for benchmark
69. remove SpecCheck; it is now part of the AFP

Summary

1. compile
2. more realistic timeout: 50min CPU time;
3. Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending on Finitely_Generated_Abelian_Groups
4. new entry Finitely_Generated_Abelian_Groups
5. remove duplicate entry in metadata
6. more coherent dependencies
7. fix(Regex_Equivalence) update to new SpecCheck version
8. operations for symbolic computation of bit operations
9. fixed Proof_Strategy_Language following Isabelle/f58108b7a60c
10. SpecCheck now without _ (Regex_Equivalence is still broken)