| changeset 28522 | eacb54d9e78d |
| parent 28504 | 7ad7d7d6df47 |
| child 28559 | 55c003a5600a |
--- a/NEWS Tue Oct 07 16:07:30 2008 +0200 +++ b/NEWS Tue Oct 07 16:07:33 2008 +0200 @@ -91,6 +91,11 @@ *** HOL *** +* Unified theorem tables of both code code generators. Thus [code] +and [code func] behave identically. INCOMPATIBILITY. + +* "undefined" replaces "arbitrary" in most occurences. + * Wrapper script for remote SystemOnTPTP service allows to use sledgehammer without local ATP installation (Vampire etc.). See also ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting