--- a/ProgTutorial/FirstSteps.thy	Wed Apr 08 10:40:16 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 08 13:42:18 2009 +0100
@@ -38,7 +38,7 @@
 \end{graybox}
 \end{isabelle}
 
-  Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
+  Like normal Isabelle scripts, \isacommand{ML}-commands can be
   evaluated by using the advance and undo buttons of your Isabelle
   environment. The code inside the \isacommand{ML}-command can also contain
   value and function bindings, for example

--- a/ProgTutorial/Intro.thy	Wed Apr 08 10:40:16 2009 +0100
+++ b/ProgTutorial/Intro.thy	Wed Apr 08 13:42:18 2009 +0100
@@ -1,9 +1,7 @@
 theory Intro
 imports Base
-
 begin
 
-
 chapter {* Introduction *}
 
 text {*
@@ -12,10 +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. 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 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.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -53,10 +53,10 @@
   the process of being updated.
   \end{description}
 
-  Then of course there is:
+  Then of course there are:
 
   \begin{description}
-  \item[The code.] It is the ultimate reference for how
+  \item[The Isabelle sources.] They are the ultimate reference for how
   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
@@ -99,7 +99,7 @@
   The user-level commands of Isabelle (i.e., the non-ML code) are written
   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
   \isacommand{foobar} and so on).  We use @{text "$ \<dots>"} to indicate that a
-  command needs to be run in a Unix-shell, for example:
+  command needs to be run in a UNIX-shell, for example:
 
   @{text [display] "$ grep -R ThyOutput *"}
 
@@ -127,15 +127,15 @@
   times.) The most important conventions are:
 
   \begin{itemize}
-  \item @{text t}, @{text u} for (raw) terms, @{ML_type term}
-  \item @{text ct}, @{text cu} for certified terms, @{ML_type cterm}
-  \item @{text "ty"}, @{text T}, @{text U} for (raw) types, @{ML_type typ}
-  \item @{text th}, @{text thm} for theorems, @{ML_type thm}
-  \item @{text "foo_tac"} for tactics, @{ML_type tactic}
-  \item @{text thy} for theories, @{ML_type theory}
-  \item @{text ctxt} for proof contexts, @{ML_type Proof.context}
-  \item @{text lthy} for local theories, @{ML_type local_theory}
-  \item @{text context} for generic contextx, @{ML_type Context.generic}
+  \item @{text t}, @{text u} 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}
+  \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
+  \item @{text thy} for theories; ML-type: @{ML_type theory}
+  \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}
   \end{itemize}
 *}
 

Binary file progtutorial.pdf has changed