# HG changeset patch
# User wenzelm
# Date 1154609615 -7200
# Node ID 99b6e2900c0f354de76c57c4f0f999fc914e64fd
# Parent  0f904a66eb75cca671888a667c10b09c67d0d763
updated;

diff -r 0f904a66eb75 -r 99b6e2900c0f doc-src/IsarImplementation/Thy/document/tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Wed Aug 02 23:09:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Thu Aug 03 14:53:35 2006 +0200
@@ -196,9 +196,9 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
-\verb|  (thm list -> tactic) -> thm| \\
+\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
   \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
-\verb|  (thm list -> tactic) -> thm list| \\
+\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
   \indexml{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
 \verb|  (thm list -> tactic) -> thm| \\
   \end{mldecls}
diff -r 0f904a66eb75 -r 99b6e2900c0f doc-src/IsarImplementation/Thy/tactic.thy
--- a/doc-src/IsarImplementation/Thy/tactic.thy	Wed Aug 02 23:09:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy	Thu Aug 03 14:53:35 2006 +0200
@@ -155,9 +155,9 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
-  (thm list -> tactic) -> thm"} \\
+  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
   @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
-  (thm list -> tactic) -> thm list"} \\
+  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
   @{index_ML Goal.prove_global: "theory -> string list -> term list -> term ->
   (thm list -> tactic) -> thm"} \\
   \end{mldecls}