equal
deleted
inserted
replaced
88 demanding keyword 'by' and supporting the full method expression |
88 demanding keyword 'by' and supporting the full method expression |
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 |
|
94 * Unified theorem tables of both code code generators. Thus [code] |
|
95 and [code func] behave identically. INCOMPATIBILITY. |
|
96 |
|
97 * "undefined" replaces "arbitrary" in most occurences. |
93 |
98 |
94 * Wrapper script for remote SystemOnTPTP service allows to use |
99 * Wrapper script for remote SystemOnTPTP service allows to use |
95 sledgehammer without local ATP installation (Vampire etc.). See also |
100 sledgehammer without local ATP installation (Vampire etc.). See also |
96 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
101 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
97 variable. |
102 variable. |