# HG changeset patch
# User wenzelm
# Date 1248607272 -7200
# Node ID 3689b647356d3fca8bc0dda94321639823931235
# Parent  2bd8ab91a426776be84c79fb5abe8843b101975c
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;

diff -r 2bd8ab91a426 -r 3689b647356d doc-src/IsarImplementation/Thy/Proof.thy
--- 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}
diff -r 2bd8ab91a426 -r 3689b647356d doc-src/IsarImplementation/Thy/Tactic.thy
--- 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"}.
diff -r 2bd8ab91a426 -r 3689b647356d doc-src/IsarImplementation/Thy/document/Proof.tex
--- 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}
diff -r 2bd8ab91a426 -r 3689b647356d doc-src/IsarImplementation/Thy/document/Tactic.tex
--- 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}.