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