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