# HG changeset patch
# User wenzelm
# Date 1129651163 -7200
# Node ID fddb41d3cfa5ee7b02bd832f92505482d24ab757
# Parent  29391114c295b7b1fa1049ba9bc20ba412049e14
Simplifier.context/theory_context;

diff -r 29391114c295 -r fddb41d3cfa5 NEWS
--- 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.
+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