--- a/ProgTutorial/Intro.thy	Mon Jun 18 15:04:34 2012 +0100
+++ b/ProgTutorial/Intro.thy	Mon Jun 18 16:46:38 2012 +0100
@@ -293,9 +293,6 @@
   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   about parsing.
 
-  \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
-  @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. 
-
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 
   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
@@ -310,6 +307,9 @@
 
   \item {\bf Christian Sternagel} proofread the tutorial and made 
   many improvemets to the text. 
+
+  \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
+  @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining

--- a/ProgTutorial/Parsing.thy	Mon Jun 18 15:04:34 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Jun 18 16:46:38 2012 +0100
@@ -980,21 +980,21 @@
   the name for the command, a kind indicator, a short description and 
   a parser producing a local theory transition (explained later). For the
   name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
-  After this, you can write in your theory 
+  You can now write in your theory 
 *}
 
 foobar
 
 text {*
-  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).
+  but of course you will not see anything since \isacommand{foobar} is
+  not intended to do anything.  Remember, however, 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 in the theory header as
+  As it stands, 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 \isacommand{foobar\_trace} in the theory header as
 
   \begin{graybox}
   \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
@@ -1091,31 +1091,33 @@
 
 text {*
   The last command we describe here is
-  \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
+  \isacommand{foobar\_proof}. Like \isacommand{foobar\_goal}, 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 a
+  \isacommand{foobar\_goal}, the proposition will be given as a
   ML-value. Such a command is quite useful during development
   when you generate a goal on the ML-level and want to see
-  whether it is provable. In addition allow the proved 
+  whether it is provable. In addition we want to allow the proved 
   proposition to have a name that can be referenced later on.
 
-  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.
+  The first problem for \isacommand{foobar\_proof} is to parse some
+  text as ML-source and then interpret it as an Isabelle term using
+  the ML-runtime.  For the parsing part, 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.
 *}
 
 ML %grayML{*
-structure Result = Proof_Data (
-  type T = unit -> term
-  fun init thy () = error "Result")
+structure Result = 
+  Proof_Data (type T = unit -> term
+              fun init thy () = error "Result")
 
 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 implement the code for \isacommand{foobar\_prove} 
+  as follows.
 *}
 
 ML %linenosgray{*let
@@ -1142,8 +1144,8 @@
   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 given name @{text "thm_name"}.
+  function @{text "after_qed"} as argument, whose purpose is to store the theorem
+  (once it is proven) under the given name @{text "thm_name"}.
 
   You can now define a term, for example
 *}
@@ -1159,7 +1161,7 @@
 done
 
 text {*
-  Finally we can test whether the lemma has been stored under the given name.
+  Finally you can test whether the lemma has been stored under the given name.
   
   \begin{isabelle}
   \isacommand{thm}~@{text "test"}\\
@@ -1313,12 +1315,13 @@
   @{text "thy_goal"} say,  you need to recreate the keyword file.
 *}
 
+
+
+
 text {*
   {\bf TBD below}
 
-  (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
-  
-*}
+ *}
 
 
 

Binary file progtutorial.pdf has changed