--- a/ProgTutorial/Parsing.thy	Tue Mar 24 09:34:03 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Mar 24 12:09:38 2009 +0100
@@ -563,6 +563,8 @@
   Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
 *}
 
+section {* Argument and Attribute Parsers (TBD) *}
+
 section {* Parsing Inner Syntax *}
 
 text {*
@@ -722,9 +724,11 @@
 
 text_raw {*
   \begin{exercise}
-  If you look closely how @{ML SpecParse.where_alt_specs} is implemented
-  in file @{ML_file "Pure/Isar/spec_parse.ML"} and compare it to our @{ML "spec_parser"}, 
-  you can notice an additional ``tail'' (Lines 8 to 10):
+  Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
+  in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
+  to the ``where-part'' of the introduction rules given above. Below
+  we paraphrase the code of @{ML SpecParse.where_alt_specs} adapted to our
+  purposes. 
   \begin{isabelle}
 *}
 ML %linenosgray{*val spec_parser' = 
@@ -739,14 +743,16 @@
                   OuterParse.!!! (OuterParse.$$$ "|"))))) [] *}
 text_raw {*
   \end{isabelle}
-  What is the purpose of this additional ``tail''?
+  Both parsers accept the same input, but if you look closely, you can notice 
+  an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of 
+  this additional ``tail''?
   \end{exercise}
 *}
 
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*
-  (FIXME: update to the right command setup)
+  (FIXME: update to the right command setup --- is this still needed)
 
   Often new commands, for example for providing new definitional principles,
   need to be implemented. While this is not difficult on the ML-level,
@@ -847,7 +853,7 @@
   You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
   and add the line 
 
-  @{text [display] "use_thy \"Command\";"} 
+  @{text [display] "no_document use_thy \"Command\";"} 
   
   to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
 
@@ -1005,27 +1011,33 @@
 section {* Methods *}
 
 text {*
-  Methods are a central concept in Isabelle. They are the ones you use for example
+  (FIXME: maybe move to after the tactic section)
+
+  Methods are a central to Isabelle. They are the ones you use for example
   in \isacommand{apply}. To print out all currently known methods you can use the 
   Isabelle command:
-*}
 
-print_methods
+  \begin{isabelle}
+  \isacommand{print\_methods}\\
+  @{text "> methods:"}\\
+  @{text ">   -:  do nothing (insert current facts only)"}\\
+  @{text ">   HOL.default:  apply some intro/elim rule (potentially classical)"}\\
+  @{text ">   ..."}
+  \end{isabelle}
 
-text {*
   An example of a very simple method is:
 *}
 
 method_setup %gray foobar_meth = 
  {* Scan.succeed
       (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
-         "foobar method"
+         "foobar method for conjE and conjI"
 
 text {*
   It defines the method @{text foobar_meth}, which takes no arguments (therefore the
-  parser @{ML Scan.succeed}) and 
-  only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}.
-  This method can be used in the following proof
+  parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which 
+  applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD}
+  turns such a tactic into a method. @{text "Foobar_meth"} can be used as follows
 *}
 
 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"