--- a/doc-src/IsarImplementation/Thy/Proof.thy Sun Jul 26 13:12:54 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Sun Jul 26 13:21:12 2009 +0200
@@ -95,7 +95,7 @@
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{index_ML Variable.import: "bool -> thm list -> Proof.context ->
((ctyp list * cterm list) * thm list) * Proof.context"} \\
- @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
+ @{index_ML Variable.focus: "cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context"} \\
\end{mldecls}
\begin{description}
@@ -284,10 +284,7 @@
text %mlref {*
\begin{mldecls}
- @{index_ML SUBPROOF:
- "({context: Proof.context, schematics: ctyp list * cterm list,
- params: cterm list, asms: cterm list, concl: cterm,
- prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
+ @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
@@ -297,7 +294,7 @@
\end{mldecls}
\begin{mldecls}
@{index_ML Obtain.result: "(Proof.context -> tactic) ->
- thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
+ thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jul 26 13:12:54 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jul 26 13:21:12 2009 +0200
@@ -63,7 +63,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML Goal.init: "cterm -> thm"} \\
- @{index_ML Goal.finish: "thm -> thm"} \\
+ @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
@{index_ML Goal.protect: "thm -> thm"} \\
@{index_ML Goal.conclude: "thm -> thm"} \\
\end{mldecls}
@@ -73,9 +73,10 @@
\item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
the well-formed proposition @{text C}.
- \item @{ML "Goal.finish"}~@{text "thm"} checks whether theorem
+ \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
@{text "thm"} is a solved goal (no subgoals), and concludes the
- result by removing the goal protection.
+ result by removing the goal protection. The context is only
+ required for printing error messages.
\item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
of theorem @{text "thm"}.
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sun Jul 26 13:12:54 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sun Jul 26 13:21:12 2009 +0200
@@ -113,7 +113,7 @@
\indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
\indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
- \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
+ \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\
\end{mldecls}
\begin{description}
@@ -324,9 +324,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
-\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
-\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
@@ -336,7 +334,7 @@
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
-\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
+\verb| thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Sun Jul 26 13:12:54 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Sun Jul 26 13:21:12 2009 +0200
@@ -84,7 +84,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
- \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: thm -> thm| \\
+ \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: Proof.context -> thm -> thm| \\
\indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
\indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
\end{mldecls}
@@ -94,9 +94,10 @@
\item \verb|Goal.init|~\isa{C} initializes a tactical goal from
the well-formed proposition \isa{C}.
- \item \verb|Goal.finish|~\isa{thm} checks whether theorem
+ \item \verb|Goal.finish|~\isa{ctxt\ thm} checks whether theorem
\isa{thm} is a solved goal (no subgoals), and concludes the
- result by removing the goal protection.
+ result by removing the goal protection. The context is only
+ required for printing error messages.
\item \verb|Goal.protect|~\isa{thm} protects the full statement
of theorem \isa{thm}.