--- a/ProgTutorial/Intro.thy	Fri Jul 31 19:10:39 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sat Aug 01 08:59:41 2009 +0200
@@ -57,8 +57,7 @@
   useful.
 
   \item[The Isar Reference Manual] provides specification material (like grammars,
-  examples and so on) about Isar and its implementation. It is currently in
-  the process of being updated.
+  examples and so on) about Isar and its implementation.
   \end{description}
 
   Then of course there are:
@@ -152,8 +151,8 @@
   is to get your code into the Isabelle distribution. For this you have
   to convince other developers that your code or project is of general interest. 
   If you managed to do this, then the problem of the moving target goes 
-  away, because when checking in code, developers are strongly urged to 
-  test against Isabelle's code base. If your project is part of that code base, 
+  away, because when checking in new code, developers are strongly urged to 
+  test it against Isabelle's code base. If your project is part of that code base, 
   then maintenance is done by others. Unfortunately, this might not
   be a helpful advice for all types of projects. A lower threshold for inclusion has the 
   Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}}
@@ -165,6 +164,7 @@
   with checking agains the distribution, but generally problems will be caught
   and the developer, who caused them, is expected to fix them. So also
   in this case code maintenance is done for you. 
+
 *}
 
 section {* Some Naming Conventions in the Isabelle Sources *}