# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259179231 -3600
# Node ID 3d27d77c351f3c2bd5685965382434ebc68d3b24
# Parent  444bc9f17cfccf302ef3644e36aa870e6bdacedd
added RANGE

diff -r 444bc9f17cfc -r 3d27d77c351f ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue Nov 24 22:55:44 2009 +0100
+++ b/ProgTutorial/Essential.thy	Wed Nov 25 21:00:31 2009 +0100
@@ -1885,8 +1885,12 @@
   @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
   \end{isabelle}
 
-  Such theorem styles allow one to print out theorems in documents formatted to
-  ones heart content. Next we explain theorem attributes, which is another
+  Such styles allow one to print out theorems in documents formatted to 
+  ones heart content. The styles can also be used in the document 
+  antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"}
+  and @{text "@{typeof ...}"}.
+
+  Next we explain theorem attributes, which is another
   mechanism for dealing with theorems.
 
   \begin{readmore}
diff -r 444bc9f17cfc -r 3d27d77c351f ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Tue Nov 24 22:55:44 2009 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Wed Nov 25 21:00:31 2009 +0100
@@ -86,10 +86,10 @@
   \begin{center}\small
   \mprset{flushleft}
   \mbox{\inferrule{
-             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
-            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
+             @{thm (prem1)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm (prem2)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm (prem3)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
+            {@{thm (concl)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
   \end{center}
 
   But this does not correspond to the induction principle we derived by hand, which
diff -r 444bc9f17cfc -r 3d27d77c351f ProgTutorial/Tactical.thy
--- 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}, 
diff -r 444bc9f17cfc -r 3d27d77c351f progtutorial.pdf
Binary file progtutorial.pdf has changed