# HG changeset patch
# User wenzelm
# Date 1372322137 -7200
# Node ID c45a6939217f919705d6e45ac0361191cce9133d
# Parent  a241826ed00328787867c8df225ace75b38bc1d1
updated documentation;

diff -r a241826ed003 -r c45a6939217f NEWS
--- a/NEWS	Thu Jun 27 10:14:17 2013 +0200
+++ b/NEWS	Thu Jun 27 10:35:37 2013 +0200
@@ -68,6 +68,10 @@
 * Discontinued empty name bindings in 'axiomatization'.
 INCOMPATIBILITY.
 
+* SELECT_GOAL now retains the syntactic context of the overall goal
+state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
+situations.
+
 
 *** HOL ***
 
diff -r a241826ed003 -r c45a6939217f src/Doc/IsarImplementation/Proof.thy
--- a/src/Doc/IsarImplementation/Proof.thy	Thu Jun 27 10:14:17 2013 +0200
+++ b/src/Doc/IsarImplementation/Proof.thy	Thu Jun 27 10:35:37 2013 +0200
@@ -387,7 +387,6 @@
 
 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) ->
@@ -414,10 +413,6 @@
 
   \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 a241826ed003 -r c45a6939217f src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 10:14:17 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 10:35:37 2013 +0200
@@ -179,6 +179,8 @@
   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
+  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
+  @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
   \end{mldecls}
 
   \begin{description}
@@ -218,6 +220,16 @@
   avoids expensive re-certification in situations where the subgoal is
   used directly for primitive inferences.
 
+  \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
+  specified subgoal @{text "i"}.  This rearranges subgoals and the
+  main goal protection (\secref{sec:tactical-goals}), while retaining
+  the syntactic context of the overall goal state (concerning
+  schematic variables etc.).
+
+  \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
+  @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but
+  without changing the main goal protection.
+
   \end{description}
 *}