summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 04 Jan 2006 01:00:52 +0100 | |

changeset 18567 | ecdd71518f33 |

parent 18566 | 20dd2f7dca4b |

child 18568 | 0728c4c38b62 |

* Pure/Isar: Toplevel.theory_theory_to_proof;

--- a/NEWS Wed Jan 04 00:52:49 2006 +0100 +++ b/NEWS Wed Jan 04 01:00:52 2006 +0100 @@ -279,12 +279,16 @@ slightly more general idea of ``protecting'' meta-level rule statements. -* Pure/goals: structure Goal provides simple interfaces for +* Pure: structure Goal provides simple interfaces for init/conclude/finish and tactical prove operations (replacing former Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been obsolete, it is ill-behaved in a local proof context (e.g. with local fixes/assumes or in a locale context). +* Pure/Isar: Toplevel.theory_theory_to_proof admits transactions that +modify the theory before entering a proof state, i.e. the composition +of Toplevel.theory and Toplevel.theory_to_proof. + * 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