--- 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)
----------------------------------