# 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.