doc-src/IsarImplementation/Thy/Proof.thy

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