# HG changeset patch
# User wenzelm
# Date 1152356068 -7200
# Node ID 2308529f8e8dc1aac74b236affdca74c080b1883
# Parent  ae7aba935986d3d7be734a9d6dc210bbf0eeb84e
updated Goal.prove, Goal.prove_global;

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}
 *}