* Simplifier: simpset of a running simplification process contains a proof context;
* Simplifier.inherit_context supercedes Simplifier.inherit_bounds;
* Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;

--- a/NEWS	Mon Oct 17 23:10:24 2005 +0200
+++ b/NEWS	Mon Oct 17 23:10:25 2005 +0200
@@ -55,7 +55,7 @@
 * 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
+simpset_of/local_simpset_of).  Consequently, all plug-in complements
 (solver, looper etc.) may depend on arbitrary proof data.
 
 * Simplifier.inherit_context inherits the proof context (plus the