diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/Intro.thy	Mon Aug 03 16:47:01 2009 +0200
@@ -175,7 +175,7 @@
   times.) The most important conventions are:
 
   \begin{itemize}
-  \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term}
+  \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
   \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
   \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
   \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}