--- a/ProgTutorial/Essential.thy	Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/Essential.thy	Thu Nov 17 16:33:49 2011 +0000
@@ -115,12 +115,13 @@
 end"
 "?x3, ?x1.3, x"}
 
-  When constructing terms, you are usually concerned with free variables (as
-  mentioned earlier, you cannot construct schematic variables using the
-  antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
-  however, observe the distinction. The reason is that only schematic
-  variables can be instantiated with terms when a theorem is applied. A
-  similar distinction between free and schematic variables holds for types
+  When constructing terms, you are usually concerned with free
+  variables (as mentioned earlier, you cannot construct schematic
+  variables using the built in antiquotation \mbox{@{text "@{term
+  \<dots>}"}}). If you deal with theorems, you have to, however, observe the
+  distinction. The reason is that only schematic variables can be
+  instantiated with terms when a theorem is applied. A similar
+  distinction between free and schematic variables holds for types
   (see below).
 
   \begin{readmore}
@@ -1555,8 +1556,10 @@
   While we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
-  by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
-  to the section about local-setup is given here.}
+  by using the function @{ML_ind note in Local_Theory} from the structure 
+  @{ML_struct Local_Theory} (the Isabelle command
+  \isacommand{local\_setup} will be explained in more detail in 
+  Section~\ref{sec:local}).
 *}
 
 local_setup %gray {*
@@ -1598,7 +1601,7 @@
   [source] my_thm_simp} is that they can now also be referenced with the
   \isacommand{thm}-command on the user-level of Isabelle
 
-
+    
   \begin{isabelle}
   \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
   @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
@@ -2009,16 +2012,20 @@
   using @{text "@{thm \<dots>}"} produces
 
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm style_test}"}\\
   @{text ">"}~@{thm style_test}
+  \end{graybox}
   \end{isabelle}
 
   as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 
   we obtain
 
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm (my_strip_allq) style_test}"}\\
   @{text ">"}~@{thm (my_strip_allq) style_test}
+  \end{graybox}
   \end{isabelle}
   
   without the leading quantifiers. We can improve this theorem style by explicitly 
@@ -2051,10 +2058,11 @@
   on the resulting term. We can now suggest, for example, two variables for
   stripping off the first two @{text \<forall>}-quantifiers.
 
-
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
   @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
+  \end{graybox}
   \end{isabelle}
 
   Such styles allow one to print out theorems in documents formatted to