# HG changeset patch
# User wenzelm
# Date 1121362140 -7200
# Node ID 6468a5d6a16e55854b2d209c5d82906e4b93bc33
# Parent  7563d0eb341419fbd374e26c44cb9023bd09b894
* Improved 'oracle' command -- type-safe;

diff -r 7563d0eb3414 -r 6468a5d6a16e NEWS
--- 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.