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