changeset 425 | ce43c04d227d |
parent 421 | 620a24bf954a |
child 427 | 94538ddcac9b |
--- 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} *}