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