doc-src/IsarImplementation/Thy/document/proof.tex
changeset 21827 0b1d07f79c1e
parent 20797 c1f0bc7e7d80
child 22568 ed7aa5a350ef
--- 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