--- a/NEWS Thu Sep 18 14:06:58 2008 +0200
+++ b/NEWS Thu Sep 18 19:39:44 2008 +0200
@@ -22,6 +22,13 @@
*** Pure ***
+* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
+to 'a -> thm, at the cost of internal tagging of results with an
+authentic oracle name. The Isar command 'oracle' is now polymorphic,
+no argument type is specified. INCOMPATIBILITY, need to simplify
+existing oracle code accordingly. Note that extra performance may be
+gained by producing the cterm carefully, not via Thm.cterm_of.
+
* Changed defaults for unify configuration options:
unify_trace_bound = 50 (formerly 25)