# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274727731 -3600
# Node ID ce43c04d227d3bfb7dc9ed65bc43ed648ac3ddd2
# Parent  5e0a2b50707ea47a3082a89b193b784cd28feab9
added phi for morphisms

diff -r 5e0a2b50707e -r ce43c04d227d ProgTutorial/Intro.thy
--- 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}
 *}
 
diff -r 5e0a2b50707e -r ce43c04d227d progtutorial.pdf
Binary file progtutorial.pdf has changed