doc-src/IsarImplementation/Thy/document/proof.tex

   it.  The latter may depend on the local assumptions being presented
   as facts.  The result is in HHF normal form.
 
   \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
   variables and assumptions in the context.  Final results need to be
   exported explicitly.