doc-src/IsarImplementation/Thy/proof.thy
changeset 21827 0b1d07f79c1e
parent 20797 c1f0bc7e7d80
child 22568 ed7aa5a350ef
--- a/doc-src/IsarImplementation/Thy/proof.thy	Wed Dec 13 15:47:37 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Wed Dec 13 16:26:45 2006 +0100
@@ -318,8 +318,8 @@
 
   \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
   states several conclusions simultaneously.  The goal is encoded by
-  means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn
-  this into a collection of individual subgoals.
+  means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
+  into a collection of individual subgoals.
 
   \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
   given facts using a tactic, which results in additional fixed