972   Here you have to specify the subgoal of interest only once and

   972   Here you have to specify the subgoal of interest only once and it is

   973   it is consistently applied to the component.

   973   consistently applied to the component.  For most tactic combinators such a

   974   For most tactic combinators such a ``primed'' version exists and

   974   ``primed'' version exists and in what follows we will usually prefer it over

   975   in what follows we will usually prefer it over the ``unprimed'' one. 

   975   the ``unprimed'' one.

   976 

   976 

   977   If there is a list of tactics that should all be tried out in 

   977   The tactic combinator @{ML_ind RANGE in Tactical} takes a list of @{text n}

   978   sequence, you can use the combinator @{ML_ind  EVERY' in Tactical}. For example

   978   tactics, say, and applies them to each of the first @{text n} subgoals. 

   979   the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 

   979   For example below we first apply the introduction rule for conjunctions

   980   be written as:

   980   and then apply a tactic to each of the two subgoals. 

   981 *}

   982 

   983 lemma 

   984   shows "A \<Longrightarrow> True \<and> A"

   985 apply(tactic {* (rtac @{thm conjI} 

   986                  THEN' RANGE [rtac @{thm TrueI}, atac]) 1 *})

   987 txt {* \begin{minipage}{\textwidth}

   988        @{subgoals [display]} 

   989        \end{minipage} *}

   990 (*<*)oops(*>*)

   991 

   992 text {*

   993   If there is a list of tactics that should all be tried out in sequence on

   994   one specified subgoal, you can use the combinator @{ML_ind EVERY' in

   995   Tactical}. For example the function @{ML foo_tac'} from

   996   page~\pageref{tac:footacprime} can also be written as: