# HG changeset patch
# User wenzelm
# Date 1221761522 -7200
# Node ID 3ba048423a99ad7f049cd0c999e2d3d6baf9a042
# Parent  f15c2e2ffe1b2f317383f9163d69c56c8947a38a
tuned;

diff -r f15c2e2ffe1b -r 3ba048423a99 NEWS
--- a/NEWS	Thu Sep 18 19:39:50 2008 +0200
+++ b/NEWS	Thu Sep 18 20:12:02 2008 +0200
@@ -22,13 +22,6 @@
 
 *** 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)
@@ -216,6 +209,13 @@
 
 *** ML ***
 
+* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
+to 'a -> thm, while results are always tagged 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, avoiding slow Thm.cterm_of.
+
 * ML bindings produced via Isar commands are stored within the Isar
 context (theory or proof).  Consequently, commands like 'use' and 'ML'
 become thread-safe and work with undo as expected (concerning