--- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Wed Jan 11 00:11:02 2006 +0100
@@ -181,8 +181,6 @@
\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-theory-to-proof}\verb|Toplevel.theory_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%
@@ -205,13 +203,10 @@
\item \verb|Toplevel.theory| adjoins a theory transformer.
\item \verb|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 \verb|Toplevel.theory_theory_to_proof| is like \verb|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 \verb|Toplevel.proof| adjoins a deterministic proof command,
with a singleton result state.