--- a/ProgTutorial/Intro.thy	Mon May 17 18:20:48 2010 +0100
+++ b/ProgTutorial/Intro.thy	Mon May 24 20:02:11 2010 +0100
@@ -226,6 +226,7 @@
   \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}
+  \item @{text phi} for morphisms; ML-type @{ML_type morphism}
   \end{itemize}
 *}
 

Binary file progtutorial.pdf has changed