--- a/ProgTutorial/Advanced.thy	Wed Nov 09 10:16:23 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Wed Nov 09 20:57:15 2011 +0000
@@ -41,7 +41,8 @@
   must be stored in a theory in order to be usable later on. Similar
   with proofs: once a proof is finished, the proved theorem needs to
   be stored in the theorem database of the theory in order to be
-  usable. All relevant data of a theory can be queried as follows.
+  usable. All relevant data of a theory can be queried with the
+  Isabelle command \isacommand{print\_theory}.
 
   \begin{isabelle}
   \isacommand{print\_theory}\\
@@ -62,21 +63,21 @@
   Functions acting on theories often end with the suffix @{text "_global"},
   for example the function @{ML read_term_global in Syntax} in the structure
   @{ML_struct Syntax}. The reason is to set them syntactically apart from
-  functions acting on contexts or local theories (which will be discussed in
-  the next sections). There is a tendency in the Isabelle development to prefer
+  functions acting on contexts or local theories, which will be discussed in
+  the next sections. There is a tendency amongst Isabelle developers to prefer
   ``non-global'' operations, because they have some advantages, as we will also
   discuss later. However, some basic understanding of theories is still necessary
   for effective Isabelle programming.
 
-  An important command with theories is \isacommand{setup}. In the
+  An important Isabelle command with theories is \isacommand{setup}. In the
   previous chapters we used it to make, for example, a theorem attribute known
   to Isabelle or to register a theorem under a name. What happens behind the
   scenes is that \isacommand{setup} expects a function of type @{ML_type
   "theory -> theory"}: the input theory is the current theory and the output
   the theory where the attribute has been registered or the theorem has been
   stored.  This is a fundamental principle in Isabelle. A similar situation
-  arises with declaring constants. The function that declares a constant on
-  the ML-level is @{ML_ind declare_const in Sign} in the structure @{ML_struct
+  arises with declaring a constant, which can be done on the ML-level with 
+  function @{ML_ind declare_const in Sign} from the structure @{ML_struct
   Sign}. To see how \isacommand{setup} works, consider the following code:
 
 *}  
@@ -91,7 +92,7 @@
 text {*
   If you simply run this code\footnote{Recall that ML-code needs to be enclosed in
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the
-  intention of declaring a constant @{text "BAR"} with type @{typ nat}, then 
+  intention of declaring a constant @{text "BAR"} having type @{typ nat}, then 
   indeed you obtain a theory as result. But if you query the
   constant on the Isabelle level using the command \isacommand{term}
 
@@ -125,10 +126,11 @@
 
   returns now a (black) constant with the type @{typ nat}, as expected.
 
-  In a sense, \isacommand{setup} can be seen as a transaction that takes the
-  current theory, applies an operation, and produces a new current theory. This
-  means that we have to be careful to apply operations always to the most current
-  theory, not to a \emph{stale} one. Consider again the function inside the
+  In a sense, \isacommand{setup} can be seen as a transaction that
+  takes the current theory @{text thy}, applies an operation, and
+  produces a new current theory @{text thy'}. This means that we have
+  to be careful to apply operations always to the most current theory,
+  not to a \emph{stale} one. Consider again the function inside the
   \isacommand{setup}-command:
 
   \begin{isabelle}
@@ -201,16 +203,24 @@
   mundane operations like printing out a term make essential use of contexts.
   For this consider the following contrived proof whose only purpose is to 
   fix two variables:
+
+  \def\shadecolor{gray}
+  \begin{shaded}
+  aaa
+  \end{shaded}
+
+  \mbox{}\hspace{10mm}\begin{graybox}aa\end{graybox}
 *}
 
 lemma "True"
 proof -
-  txt {*\mbox{}\\[-7mm]*} ML_prf {* Variable.dest_fixes @{context} *} txt {*\mbox{}\\[-7mm]*}
+  txt_raw {*\mbox{}\\[-7mm]*} 
+  ML_prf{*Variable.dest_fixes @{context}*} 
+  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
   fix x y  
-  txt {*\mbox{}\\[-7mm]*}
+  txt_raw {*\mbox{}\\[-7mm]*}
   ML_prf {* Variable.dest_fixes @{context} *} 
-  txt {*\mbox{}\\[-7mm]*}
-oops
+  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
 
 text {*
   The interesting point in this proof is that we injected ML-code before and after
@@ -231,14 +241,17 @@
 proof -
   fix x y
   { fix z w
-  txt {*\mbox{}\\[-7mm]*}
+  txt_raw {*\mbox{}\\[-7mm]*}
+  ML_prf {* Variable.dest_fixes @{context} *} 
+  txt_raw {*\mbox{}\\[-7mm]*}
+  txt_raw {* \mbox{}\hspace{4mm}\mbox{} *} }
+  txt_raw {*\mbox{}\\[-7mm]*}
   ML_prf {* Variable.dest_fixes @{context} *} 
-  txt {*\mbox{}\\[-7mm]*}
-     }
-  txt {*\mbox{}\\[-7mm]*}
-  ML_prf {* Variable.dest_fixes @{context} *} 
-  txt {*\mbox{}\\[-7mm]*}
-oops
+  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
+
+text {*
+  The above proof corresoponds roughly to the following ML-code.
+*}
 
 (*
 ML{*Proof_Context.debug := true*}

Binary file progtutorial.pdf has changed