--- a/ProgTutorial/First_Steps.thy	Wed Oct 26 12:59:44 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Wed Oct 26 13:18:51 2011 +0100
@@ -18,7 +18,7 @@
   ``We will most likely never realize the full importance of painting the Tower,\\ 
   that it is the essential element in the conservation of metal works and the\\ 
   more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
-  Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
+  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
   re-painted 18 times since its initial construction, an average of once every 
   seven years. It takes more than one year for a team of 25 painters to paint the tower 
   from top to bottom.}
@@ -295,7 +295,7 @@
   Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
 
 text {*
-  Printing functions for types are
+  Printing functions for @{ML_type typ} are
 *}
 
 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
@@ -303,7 +303,7 @@
   Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
 
 text {*
-  respectively ctypes
+  respectively @{ML_type ctyp}
 *}
 
 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)

--- a/ProgTutorial/Tactical.thy	Wed Oct 26 12:59:44 2011 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Oct 26 13:18:51 2011 +0100
@@ -14,9 +14,9 @@
 
 text {*
    \begin{flushright}
-  {\em ``The most effective debugging tool is still careful thought, coupled with 
-  judiciously placed print statements.''} \\[1ex]
-  Brian Kernighan 
+  {\em ``The most effective debugging tool is still careful thought,\\ 
+  coupled with judiciously placed print statements.''} \\[1ex]
+  Brian Kernighan, in {\em Unix for Beginners}, 1979
   \end{flushright}
 
   \medskip

Binary file progtutorial.pdf has changed