--- a/ProgTutorial/FirstSteps.thy	Mon Oct 19 14:10:42 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Oct 19 17:31:13 2009 +0200
@@ -714,9 +714,10 @@
   with ML-antiquotations, often just called antiquotations.\footnote{There are
   two kinds of antiquotations in Isabelle, which have very different purposes
   and infrastructures. The first kind, described in this section, are
-  \emph{ML-antiquotations}. They are used to refer to entities (like terms,
+  \emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms,
   types etc) from Isabelle's logic layer inside ML-code. The other kind of
-  antiquotations are \emph{document} antiquotations. They are used only in the
+  antiquotations are \emph{document}\index{document antiquotationa} antiquotations. 
+  They are used only in the
   text parts of Isabelle and their purpose is to print logical entities inside
   \LaTeX-documents. Document antiquotations are part of the user level and
   therefore we are not interested in them in this Tutorial, except in Appendix

--- a/ProgTutorial/General.thy	Mon Oct 19 14:10:42 2009 +0200
+++ b/ProgTutorial/General.thy	Mon Oct 19 17:31:13 2009 +0200
@@ -1129,19 +1129,19 @@
   proved theorems can be quoted in documents referencing directly their
   formalisation. This helps tremendously to minimise cut-and-paste errors. However,
   sometimes the verbatim quoting is not what is wanted or what can be shown to
-  readers. For such situations Isabelle allows the installation of \emph{theorem 
-  styles}. These are, roughly speaking, functions from terms to terms. The input 
+  readers. For such situations Isabelle allows the installation of \emph{\index*{theorem 
+  styles}}. These are, roughly speaking, functions from terms to terms. The input 
   term stands for the theorem to be presented; the output can be constructed to
   ones wishes.  Let us, for example, assume we want to quote theorems without
   leading @{text \<forall>}-quantifiers. For this we can implement the following function 
   that strips off meta-quantifiers.
 *}
 
-ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) = 
-      Term.dest_abs body |> snd |> strip_all_qnt
-  | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) = 
-      strip_all_qnt t
-  | strip_all_qnt t = t*}
+ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
+      Term.dest_abs body |> snd |> strip_allq
+  | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = 
+      strip_allq t
+  | strip_allq t = t*}
 
 text {*
   We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,
@@ -1149,11 +1149,11 @@
   a pair consisting of the variable and the body of the abstraction. We are only interested
   in the body, which we feed into the recursive call. In Line 3 and 4, we also
   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 
-  install this function as the theorem style named @{text "my_strip_all_qnt"}. 
+  install this function as the theorem style named @{text "my_strip_allq"}. 
 *}
 
 setup %gray {*
-  Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt)) 
+  Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) 
 *}
 
 text {*
@@ -1172,12 +1172,12 @@
   @{text ">"}~@{thm style_test}
   \end{isabelle}
 
-  as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \<dots>}"} 
+  as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 
   we obtain
 
   \begin{isabelle}
-  @{text "@{thm (my_strip_all_qnt) style_test}"}\\
-  @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\
+  @{text "@{thm (my_strip_allq) style_test}"}\\
+  @{text ">"}~@{thm (my_strip_allq) style_test}\\
   \end{isabelle}
   
   without the leading quantifiers. We can improve this theorem style by explicitly 
@@ -1186,12 +1186,12 @@
   and uses them as name in the outermost abstractions.
 *}
 
-ML {*fun rename_all [] t = t
-  | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
-      Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t)
-  | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) =
-      rename_all xs t
-  | rename_all _ t = t*}
+ML {*fun rename_allq [] t = t
+  | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
+      Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
+  | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
+      rename_allq xs t
+  | rename_allq _ t = t*}
 
 text {*
   We can now install a the modified theorem style as follows
@@ -1200,18 +1200,21 @@
 setup %gray {*
 let
   val parser = Scan.repeat Args.name
-  fun action xs = K (rename_all xs #> strip_all_qnt)
+  fun action xs = K (rename_allq xs #> strip_allq)
 in
-  Term_Style.setup "my_strip_all_qnt2" (parser >> action)
+  Term_Style.setup "my_strip_allq2" (parser >> action)
 end *}
 
 text {*
-  We can now suggest, for example, two variables for stripping 
-  off the @{text \<forall>}-quantifiers, namely:
+  The parser reads a list of names. In the function @{ML_text action} we first
+  call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}
+  on the resulting term. We can now suggest, for example, two variables for
+  stripping off the first two @{text \<forall>}-quantifiers.
+
 
   \begin{isabelle}
-  @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\
-  @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test}
+  @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
+  @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
   \end{isabelle}
 
   Such theorem styles allow one to print out theorems in documents formatted to

Binary file progtutorial.pdf has changed