Tue, 18 Oct 2005 17:59:23 +0200
changeset 17890 fddb41d3cfa5
parent 17889 29391114c295
child 17891 7a6c4d60a913
--- a/NEWS	Tue Oct 18 17:59:22 2005 +0200
+++ b/NEWS	Tue Oct 18 17:59:23 2005 +0200
@@ -55,14 +55,15 @@
 * 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 complements
+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.  Tools based on low-level rewriting may even have to
+specify an explicit context using Simplifier.context/theory_context.
 * Simplifier/Classical Reasoner: more abstract interfaces
 change_simpset/claset for modifying the simpset/claset reference of a