--- a/ProgTutorial/Intro.thy	Wed Apr 08 13:42:18 2009 +0100
+++ b/ProgTutorial/Intro.thy	Wed Apr 08 22:47:39 2009 +0100
@@ -10,12 +10,12 @@
   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 recent versions of Isabelle. 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 welcome! The
-  tutorial is meant to be gentle and comprehensive. To achieve this we need
-  your feedback.
+  against \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 
+  welcome! The tutorial is meant to be gentle and comprehensive. To achieve 
+  this we need your feedback.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -60,9 +60,9 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The GNU/UNIX command @{text "grep -R"} is
+  learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
   often your best friend while programming with Isabelle, or
-  hypersearch if you use jEdit under MacOSX.
+  hypersearch if you program using jEdit under MacOSX.
   \end{description}
 
 *}
@@ -136,6 +136,7 @@
   \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
   \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}
   \end{itemize}
 *}