# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1319631531 -3600
# Node ID 0fb910f62bf9db6050bd75ac7ead2c57bbcdd4e0
# Parent  25371f74c768fa127cd6d519e143a81e34c838a8
minor things

diff -r 25371f74c768 -r 0fb910f62bf9 ProgTutorial/First_Steps.thy
--- 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)
diff -r 25371f74c768 -r 0fb910f62bf9 ProgTutorial/Tactical.thy
--- 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
diff -r 25371f74c768 -r 0fb910f62bf9 progtutorial.pdf
Binary file progtutorial.pdf has changed