--- a/doc-src/IsarImplementation/Thy/integration.thy Tue Jan 03 15:44:39 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy Wed Jan 04 00:52:38 2006 +0100
@@ -136,6 +136,8 @@
Toplevel.transition -> Toplevel.transition"} \\
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.theory_to_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) ->
@@ -163,6 +165,10 @@
specifies how to apply the proven result to the theory, when the
proof is finished.
+ \item @{ML Toplevel.theory_to_theory_to_proof} is like @{ML
+ Toplevel.theory_to_proof}, but allows the initial theory to be
+ changed before entering proof state.
+
\item @{ML Toplevel.proof} adjoins a deterministic proof command,
with a singleton result state.