# HG changeset patch
# User wenzelm
# Date 1327588097 -3600
# Node ID b6ab3cdea1637a179256867c3c3b34639744437c
# Parent  f575281fb551ba02aa8b20f57b0510ea4f850228
added SELECT_GOAL;

diff -r f575281fb551 -r b6ab3cdea163 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
diff -r f575281fb551 -r b6ab3cdea163 doc-src/IsarImplementation/Thy/document/Proof.tex
--- 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