--- a/ProgTutorial/Tactical.thy	Tue Nov 24 22:55:44 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Nov 25 21:00:31 2009 +0100
@@ -969,15 +969,31 @@
 (*<*)oops(*>*)
 
 text {* 
-  Here you have to specify the subgoal of interest only once and
-  it is consistently applied to the component.
-  For most tactic combinators such a ``primed'' version exists and
-  in what follows we will usually prefer it over the ``unprimed'' one. 
-
-  If there is a list of tactics that should all be tried out in 
-  sequence, you can use the combinator @{ML_ind  EVERY' in Tactical}. For example
-  the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 
-  be written as:
+  Here you have to specify the subgoal of interest only once and it is
+  consistently applied to the component.  For most tactic combinators such a
+  ``primed'' version exists and in what follows we will usually prefer it over
+  the ``unprimed'' one.
+
+  The tactic combinator @{ML_ind RANGE in Tactical} takes a list of @{text n}
+  tactics, say, and applies them to each of the first @{text n} subgoals. 
+  For example below we first apply the introduction rule for conjunctions
+  and then apply a tactic to each of the two subgoals. 
+*}
+
+lemma 
+  shows "A \<Longrightarrow> True \<and> A"
+apply(tactic {* (rtac @{thm conjI} 
+                 THEN' RANGE [rtac @{thm TrueI}, atac]) 1 *})
+txt {* \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  If there is a list of tactics that should all be tried out in sequence on
+  one specified subgoal, you can use the combinator @{ML_ind EVERY' in
+  Tactical}. For example the function @{ML foo_tac'} from
+  page~\pageref{tac:footacprime} can also be written as:
 *}
 
 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},