diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 21:16:11 2012 +0100
@@ -715,7 +715,7 @@
 %
 \endisadelimML
 %
-\isamarkupsubsection{Scanning for a subgoal by number%
+\isamarkupsubsection{Applying tactics to subgoal ranges%
 }
 \isamarkuptrue%
 %
@@ -724,7 +724,7 @@
   \verb|int -> tactic| can be used together with tacticals that
   act like ``subgoal quantifiers'': guided by success of the body
   tactic a certain range of subgoals is covered.  Thus the body tactic
-  is applied to all subgoals, for example.
+  is applied to \emph{all} subgoals, \emph{some} subgoal etc.
 
   Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals.  Many of
   these tacticals address subgoal ranges counting downwards from
@@ -746,8 +746,10 @@
   \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
   \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
   \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
+  \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
   \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\
   \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\
+  \indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\
   \end{mldecls}
 
   \begin{description}
@@ -761,12 +763,19 @@
   \item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}.  It
   applies \isa{tac} to one subgoal, counting upwards.
 
+  \item \verb|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}.
+  It applies \isa{tac} unconditionally to the first subgoal.
+
   \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or
   more to a subgoal, counting downwards.
 
   \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or
   more to a subgoal, counting upwards.
 
+  \item \verb|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to
+  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}.  It applies the given list of tactics to the
+  corresponding range of subgoals, counting downwards.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%