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