89 syntax just like the Isar command 'by'. |
89 syntax just like the Isar command 'by'. |
90 |
90 |
91 |
91 |
92 *** HOL *** |
92 *** HOL *** |
93 |
93 |
94 * Unified theorem tables for both code code generators. Thus [code func] |
94 * Unified theorem tables for both code code generators. Thus |
95 has disappeared and only [code] remains. INCOMPATIBILITY. |
95 [code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
96 |
96 |
97 * "undefined" replaces "arbitrary" in most occurences. |
97 * Constant "undefined" replaces "arbitrary" in most occurences. |
98 |
98 |
99 * Wrapper script for remote SystemOnTPTP service allows to use |
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 |
|
101 long-lived operations due to garbage collection. New thread |
|
102 based-implementation also works smoothly on non-Unix platforms |
|
103 (Cygwin). Provers are no longer hardwired, but defined within the |
|
104 theory via plain ML wrapper functions. |
|
105 |
|
106 * Wrapper scripts for remote SystemOnTPTP service allows to use |
100 sledgehammer without local ATP installation (Vampire etc.). See also |
107 sledgehammer without local ATP installation (Vampire etc.). See also |
101 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
108 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
102 variable. |
109 variable. Other provers may be included via suitable ML wrappers, see |
|
110 also src/HOL/ATP_Linkup.thy. |
103 |
111 |
104 * Normalization by evaluation now allows non-leftlinear equations. |
112 * Normalization by evaluation now allows non-leftlinear equations. |
105 Declare with attribute [code nbe]. |
113 Declare with attribute [code nbe]. |
106 |
114 |
107 * Command "value" now integrates different evaluation |
115 * Command "value" now integrates different evaluation |