--- a/doc-src/IsarImplementation/Thy/document/proof.tex Wed Dec 13 15:47:37 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Wed Dec 13 16:26:45 2006 +0100
@@ -356,8 +356,8 @@
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
states several conclusions simultaneously. The goal is encoded by
- means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn
- this into a collection of individual subgoals.
+ means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this
+ into a collection of individual subgoals.
\item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
given facts using a tactic, which results in additional fixed