--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 14 22:48:37 2006 +0200
@@ -334,7 +334,7 @@
\indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
\indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
-\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context|
+\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
\end{mldecls}
\begin{description}