--- 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}
--- 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
--- 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},
Binary file progtutorial.pdf has changed