--- a/ProgTutorial/Intro.thy	Sat May 09 03:11:36 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sat May 09 13:55:25 2009 +0200
@@ -10,7 +10,7 @@
   Isabelle programming, and also explain tricks of the trade. The best way to
   get to know the ML-level of Isabelle is by experimenting with the many code
   examples included in the tutorial. The code is as far as possible checked
-  against \input{version}. If something does not work, 
+  against the Isabelle code.\footnote{\input{version}} If something does not work, 
   then please let us know. It is impossible for us to know every environment, 
   operating system or editor in which Isabelle is used. If you have comments, 
   criticism or like to add to the tutorial, please feel free---you are most 
@@ -137,6 +137,7 @@
   \item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
   \item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
   \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
+  \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
   \end{itemize}
 *}
 
@@ -154,6 +155,8 @@
   describing the package and has been helpful \emph{beyond measure} with
   answering questions about Isabelle.
 
+  \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
+
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
   He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.