# HG changeset patch # User wenzelm # Date 1136557099 -3600 # Node ID f6a553aa3d815690da24eaf6876a331173578fb8 # Parent c27c9fa9e83db66c99d66975a451b24b7522c7b0 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory; diff -r c27c9fa9e83d -r f6a553aa3d81 NEWS --- a/NEWS Thu Jan 05 22:30:00 2006 +0100 +++ b/NEWS Fri Jan 06 15:18:19 2006 +0100 @@ -285,9 +285,10 @@ 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 (essentially an atomic -composition of Toplevel.theory and Toplevel.theory_to_proof). +* Pure/Isar: Toplevel.theory_to_proof admits transactions that modify +the theory before entering a proof state. Transactions now always see +a quasi-functional intermediate checkpoint, both in interactive and +batch mode. * Simplifier: the simpset of a running simplification process now contains a proof context (cf. Simplifier.the_context), which is the diff -r c27c9fa9e83d -r f6a553aa3d81 doc-src/IsarImplementation/Thy/integration.thy --- a/doc-src/IsarImplementation/Thy/integration.thy Thu Jan 05 22:30:00 2006 +0100 +++ b/doc-src/IsarImplementation/Thy/integration.thy Fri Jan 06 15:18:19 2006 +0100 @@ -136,8 +136,6 @@ Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.theory_theory_to_proof: "(theory -> Proof.state) -> - Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) -> @@ -160,14 +158,10 @@ \item @{ML Toplevel.theory} adjoins a theory transformer. \item @{ML Toplevel.theory_to_proof} adjoins a global goal function, - which turns a theory into a proof state. The theory must not be - changed here! The generic Isar goal setup includes an argument that - specifies how to apply the proven result to the theory, when the - proof is finished. - - \item @{ML Toplevel.theory_theory_to_proof} is like @{ML - Toplevel.theory_to_proof}, but allows the initial theory to be - changed before entering proof state. + which turns a theory into a proof state. The theory may be changed + before entering the proof; the generic Isar goal setup includes an + argument that specifies how to apply the proven result to the + theory, when the proof is finished. \item @{ML Toplevel.proof} adjoins a deterministic proof command, with a singleton result state.