95 [code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
95 [code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
96 |
96 |
97 * Constant "undefined" replaces "arbitrary" in most occurences. |
97 * Constant "undefined" replaces "arbitrary" in most occurences. |
98 |
98 |
99 * Generic ATP manager for Sledgehammer, based on ML threads instead of |
99 * Generic ATP manager for Sledgehammer, based on ML threads instead of |
100 Posix processes. Avoids forking of the ML process, can be costly for |
100 Posix processes. Avoids potentially expensive forking of the ML |
101 long-lived operations due to garbage collection. New thread |
101 process. New thread-based implementation also works on non-Unix |
102 based-implementation also works smoothly on non-Unix platforms |
102 platforms (Cygwin). Provers are no longer hardwired, but defined |
103 (Cygwin). Provers are no longer hardwired, but defined within the |
103 within the theory via plain ML wrapper functions. |
104 theory via plain ML wrapper functions. |
|
105 |
104 |
106 * Wrapper scripts for remote SystemOnTPTP service allows to use |
105 * Wrapper scripts for remote SystemOnTPTP service allows to use |
107 sledgehammer without local ATP installation (Vampire etc.). See also |
106 sledgehammer without local ATP installation (Vampire etc.). See also |
108 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
107 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
109 variable. Other provers may be included via suitable ML wrappers, see |
108 variable. Other provers may be included via suitable ML wrappers, see |