--- a/NEWS Thu Jul 14 19:28:40 2005 +0200
+++ b/NEWS Thu Jul 14 19:29:00 2005 +0200
@@ -105,6 +105,12 @@
on the signature of the theory context being presently used for
parsing/printing, see also isar-ref manual.
+* Improved 'oracle' command provides a type-safe interface to turn an
+ML expression of type theory -> T -> term into a primitive rule of
+type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
+is already included here); see also FOL/ex/IffExample.thy;
+INCOMPATIBILITY.
+
* Improved internal renaming of symbolic identifiers -- attach primes
instead of base 26 numbers.