# HG changeset patch
# User wenzelm
# Date 1136332358 -3600
# Node ID 48d5419fd191cc599e6d8a44c66ce605e25ac217
# Parent  60a0f9caa0a2c51663ef654216e01adf50e9a495
more stuff;

diff -r 60a0f9caa0a2 -r 48d5419fd191 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jan 03 15:44:39 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Wed Jan 04 00:52:38 2006 +0100
@@ -181,6 +181,8 @@
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.theory-to-theory-to-proof}\verb|Toplevel.theory_to_theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
@@ -208,6 +210,9 @@
   specifies how to apply the proven result to the theory, when the
   proof is finished.
 
+  \item \verb|Toplevel.theory_to_theory_to_proof| is like \verb|Toplevel.theory_to_proof|, but allows the initial theory to be
+  changed before entering proof state.
+
   \item \verb|Toplevel.proof| adjoins a deterministic proof command,
   with a singleton result state.
 
diff -r 60a0f9caa0a2 -r 48d5419fd191 doc-src/IsarImplementation/Thy/integration.thy
--- 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.