NEWS
changeset 17887 c10e68962ad3
parent 17878 5b9efe4d6b47
child 17890 fddb41d3cfa5
equal deleted inserted replaced
17886:9a4aea3a9ae1 17887:c10e68962ad3
    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 components
    58 simpset_of/local_simpset_of).  Consequently, all plug-in complements
    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