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

author | wenzelm |

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

changeset 18564 | 2b8ac8bc9719 |

parent 18563 | 1df7022eac6f |

child 18565 | 818a24371de9 |

added theory_to_theory_to_proof, which may change theory before entering the proof;
added forget_proof (from isar_thy.ML);

--- a/src/Pure/Isar/toplevel.ML Wed Jan 04 00:52:45 2006 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Jan 04 00:52:47 2006 +0100 @@ -71,7 +71,7 @@ val theory': (bool -> theory -> theory) -> transition -> transition val theory_context: (theory -> theory * Proof.context) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition - val theory_theory_to_proof: (theory -> Proof.state) -> transition -> transition + val theory_to_theory_to_proof: (theory -> Proof.state) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition @@ -295,9 +295,9 @@ (* primitive transitions *) (*Note: Recovery from stale theories is provided only for theory-level - operations via Transaction. Other node or state operations should - not touch theories at all. Interrupts are enabled only for Keep and - Transaction.*) + operations via Transaction below. Other node or state operations + should not touch theories at all. Interrupts are enabled only for + Keep, and Transaction.*) datatype trans = Reset | (*empty toplevel*) @@ -452,7 +452,7 @@ | _ => raise UNDEF)); val theory_to_proof = to_proof false; -val theory_theory_to_proof = to_proof true; +val theory_to_theory_to_proof = to_proof true; fun proofs' f = map_current (fn int => (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)