--- a/doc-src/IsarImplementation/Thy/Proof.thy Thu Jan 26 15:04:35 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Thu Jan 26 15:28:17 2012 +0100
@@ -387,6 +387,7 @@
text %mlref {*
\begin{mldecls}
+ @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
@{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
Proof.context -> int -> tactic"} \\
@{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
@@ -413,6 +414,10 @@
\begin{description}
+ \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
+ specified subgoal @{text "i"}. This introduces a nested goal state,
+ without decomposing the internal structure of the subgoal yet.
+
\item @{ML SUBPROOF}~@{text "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
--- 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