summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |