--- a/doc-src/IsarImplementation/Thy/document/integration.tex Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Sat Nov 04 19:25:39 2006 +0100
@@ -184,7 +184,7 @@
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
- \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
+ \indexml{Toplevel.end-proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\end{mldecls}
@@ -217,9 +217,9 @@
command, with zero or more result states (represented as a lazy
list).
- \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
- concluding proof command, that returns the resulting theory, after
- storing the resulting facts etc.
+ \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
+ proof command, that returns the resulting theory, after storing the
+ resulting facts in the context etc.
\end{description}%
\end{isamarkuptext}%