# HG changeset patch # User wenzelm # Date 1129583425 -7200 # Node ID c10e68962ad39728cb4624d5e69d45c82eff09e6 # Parent 9a4aea3a9ae1117ed73c5c0a40b96ebdcf3b186e * 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; diff -r 9a4aea3a9ae1 -r c10e68962ad3 NEWS --- 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