
diff -r ae7aba935986 -r 2308529f8e8d doc-src/IsarImplementation/Thy/tactic.thy
--- a/doc-src/IsarImplementation/Thy/tactic.thy	Sat Jul 08 12:54:27 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy	Sat Jul 08 12:54:28 2006 +0200
@@ -154,15 +154,17 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Goal.prove: "theory -> string list -> term list -> term ->
+  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   (thm list -> tactic) -> thm"} \\
-  @{index_ML Goal.prove_multi: "theory -> string list -> term list -> term list ->
+  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
   (thm list -> tactic) -> thm list"} \\
+  @{index_ML Goal.prove_global: "theory -> string list -> term list -> term ->
+  (thm list -> tactic) -> thm"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML Goal.prove}~@{text "thy xs As C tac"} states goal @{text
+  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
   "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
   and hypotheses @{text "As"} and applies tactic @{text "tac"} to
   solve it.  The latter may depend on the local assumptions being
@@ -181,6 +183,10 @@
   Tactic.conjunction_tac} may be used to split these into individual
   subgoals before commencing the actual proof.
 
+  \item @{ML Goal.prove_global} is a degraded version of @{ML
+  Goal.prove} for theory level goals; it includes a global @{ML
+  Drule.standard} for the result.
+
   \end{description}
 *}
 




