--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Jan 26 15:04:35 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Jan 26 15:28:17 2012 +0100
@@ -588,6 +588,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
+ \indexdef{}{ML}{SELECT\_GOAL}\verb|SELECT_GOAL: tactic -> int -> tactic| \\
\indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
\verb| Proof.context -> int -> tactic| \\
\indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
@@ -614,6 +615,10 @@
\begin{description}
+ \item \verb|SELECT_GOAL|~\isa{tac\ i} confines a tactic to the
+ specified subgoal \isa{i}. This introduces a nested goal state,
+ without decomposing the internal structure of the subgoal yet.
+
\item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure
of the specified sub-goal, producing an extended context and a
reduced goal, which needs to be solved by the given tactic. All