53 *** ML *** |
53 *** ML *** |
54 |
54 |
55 * Simplifier: the simpset of a running simplification process now |
55 * Simplifier: the simpset of a running simplification process now |
56 contains a proof context (cf. Simplifier.the_context), which is the |
56 contains a proof context (cf. Simplifier.the_context), which is the |
57 very context that the initial simpset has been retrieved from (by |
57 very context that the initial simpset has been retrieved from (by |
58 simpset_of/local_simpset_of). Consequently, all plug-in complements |
58 simpset_of/local_simpset_of). Consequently, all plug-in components |
59 (solver, looper etc.) may depend on arbitrary proof data. |
59 (solver, looper etc.) may depend on arbitrary proof data. |
60 |
60 |
61 * Simplifier.inherit_context inherits the proof context (plus the |
61 * Simplifier.inherit_context inherits the proof context (plus the |
62 local bounds) of the current simplification process; any simproc |
62 local bounds) of the current simplification process; any simproc |
63 etc. that calls the Simplifier recursively should do this! Removed |
63 etc. that calls the Simplifier recursively should do this! Removed |
64 former Simplifier.inherit_bounds, which is already included here -- |
64 former Simplifier.inherit_bounds, which is already included here -- |
65 INCOMPATIBILITY. |
65 INCOMPATIBILITY. Tools based on low-level rewriting may even have to |
|
66 specify an explicit context using Simplifier.context/theory_context. |
66 |
67 |
67 * Simplifier/Classical Reasoner: more abstract interfaces |
68 * Simplifier/Classical Reasoner: more abstract interfaces |
68 change_simpset/claset for modifying the simpset/claset reference of a |
69 change_simpset/claset for modifying the simpset/claset reference of a |
69 theory; raw versions simpset/claset_ref etc. have been discontinued -- |
70 theory; raw versions simpset/claset_ref etc. have been discontinued -- |
70 INCOMPATIBILITY. |
71 INCOMPATIBILITY. |