diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 NEWS
--- a/NEWS	Mon Oct 17 23:10:15 2005 +0200
+++ b/NEWS	Mon Oct 17 23:10:16 2005 +0200
@@ -50,6 +50,26 @@
 are no longer reserved, significant speedup.
 
 
+*** ML ***
+
+* Simplifier: the simpset of a running simplification process now
+contains a proof context (cf. Simplifier.the_context), which is the
+very context that the initial simpset has been retrieved from (by
+simpset_of/local_simpset_of).  Consequently, all plug-in components
+(solver, looper etc.) may depend on arbitrary proof data.
+
+* Simplifier.inherit_context inherits the proof context (plus the
+local bounds) of the current simplification process; any simproc
+etc. that calls the Simplifier recursively should do this!  Removed
+former Simplifier.inherit_bounds, which is already included here --
+INCOMPATIBILITY.
+
+* Simplifier/Classical Reasoner: more abstract interfaces
+change_simpset/claset for modifying the simpset/claset reference of a
+theory; raw versions simpset/claset_ref etc. have been discontinued --
+INCOMPATIBILITY.
+
+
 
 New in Isabelle2005 (October 2005)
 ----------------------------------