--- a/ProgTutorial/Intro.thy	Mon Jun 18 14:49:09 2012 +0100
+++ b/ProgTutorial/Intro.thy	Mon Jun 18 15:04:34 2012 +0100
@@ -294,7 +294,7 @@
   about parsing.
 
   \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
-  @{text "command_spec"}, which simplified the code. 
+  @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. 
 
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 

--- a/ProgTutorial/Parsing.thy	Mon Jun 18 14:49:09 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Jun 18 15:04:34 2012 +0100
@@ -964,7 +964,7 @@
   also to omit the kind entirely, in which case you declare a keyword
   (something that is part of a command).
 
-  Now you can implement \isacommand{foobar} as:
+  Now you can implement \isacommand{foobar} as follows.
 *}
 
 ML %grayML{*let
@@ -983,19 +983,18 @@
   After this, you can write in your theory 
 *}
 
-
 foobar
 
-
 text {*
-  Remember that this only works in jEdit. In order to let Proof-General 
+  but of course you will not see ``anything''.
+  Remember that this only works in jEdit. In order to enable also Proof-General 
   recognise this command, a keyword file needs to be generated (see next
   section).
 
   At the moment the command \isacommand{foobar} is not very useful. Let us
   refine it a bit next by letting it take a proposition as argument and
   printing this proposition inside the tracing buffer. We announce the
-  command as
+  command in the theory header as
 
   \begin{graybox}
   \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
@@ -1022,7 +1021,7 @@
 end *}
 
 text {*
-  The command is now \isacommand{foobar\_trace} and can be used to 
+  This command can now be used to 
   see the proposition in the tracing buffer.
 *}
 
@@ -1042,7 +1041,7 @@
   Below we show the command \isacommand{foobar\_goal} which takes a
   proposition as argument and then starts a proof in order to prove
   it. Therefore, we need to announce this command in the header 
-  as @{text "thy_goal"}
+  as @{text "thy_goal"}.
 
   \begin{graybox}
   \isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}
@@ -1091,18 +1090,18 @@
 done
 
 text {*
-  The final new command we describe is
+  The last command we describe here is
   \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
   to take a proposition and open a corresponding proof-state that
   allows us to give a proof for it. However, unlike
-  \isacommand{lemma}, the proposition will be given as an
+  \isacommand{lemma}, the proposition will be given as a
   ML-value. Such a command is quite useful during development
-  of a tool that generates a goal on the ML-level and you want to see
-  whether it is provable. In addition you also want that the proved 
-  proposition can be given a lemma name that can be referenced later on.
+  when you generate a goal on the ML-level and want to see
+  whether it is provable. In addition allow the proved 
+  proposition to have a name that can be referenced later on.
 
-  The first problem of this new command is to parse some text as 
-  ML-source and then interpret it as a term. For the parsing we can 
+  The first problem for this command is to parse some text as 
+  ML-source and then interpret it as an Isabelle term. For the parsing we can 
   use the function @{ML_ind "ML_source" in Parse} in the structure 
   @{ML_struct Parse}. For running the ML-interpreter we need the 
   following scaffolding code.
@@ -1116,7 +1115,7 @@
 val result_cookie = (Result.get, Result.put, "Result.put") *}
 
 text {*
-  With this in place we can write the code for \isacommand{foobar\_prove}.
+  With this in place, we can write the code for \isacommand{foobar\_prove}.
 *}
 
 ML %linenosgray{*let
@@ -1139,20 +1138,20 @@
 
 text {*
   In Line 12, we implement a parser that first reads in an optional lemma name (terminated 
-  by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML
-  text and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
+  by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
+  and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
   in the structure @{ML_struct Code_Runtime}.  Once the ML-text has been turned into a term, 
   the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
   function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem,
-  once it is proven, under the user given name @{text "thm_name"}.
+  once it is proven, under the given name @{text "thm_name"}.
 
-  We can now give take a term, for example
+  You can now define a term, for example
 *}
 
 ML %grayML{*val prop_true = @{prop "True"}*}
 
 text {*
-  and give a proove for it using \isacommand{foobar\_prove}:
+  and give it a proof using \isacommand{foobar\_prove}:
 *}
 
 foobar_prove test: prop_true

Binary file progtutorial.pdf has changed