--- a/CookBook/Parsing.thy	Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Feb 23 00:27:27 2009 +0000
@@ -45,11 +45,6 @@
 
   @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
 
-  The type of a parser is defined as
-
-  
-
-
   This function will either succeed (as in the two examples above) or raise the exception 
   @{text "FAIL"} if no string can be consumed. For example trying to parse
 
@@ -581,8 +576,8 @@
   "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
   "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
 
-  You can see better what is going on if you replace 
-  @{ML Position.none} by @{ML "Position.line 42"}, say:
+  This function returns an XML-tree. You can see better what is going on if
+  you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
 
 @{ML_response [display,gray]
 "let 
@@ -663,7 +658,7 @@
       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 
-  As can be seen, the result is a ``nested'' four-tuple consisting of an 
+  As you see, the result is a ``nested'' four-tuple consisting of an 
   optional locale (in this case @{ML NONE}); a list of variables with optional 
   type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this
   case there are none); and a list of rules where every rule has optionally a name and 
@@ -716,9 +711,10 @@
 "parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")"
 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"}  
 
-  Lines 5 to 9 implement the parser for a list of introduction rules, that is propositions 
-  with theorem annotations. The introduction rules are propositions parsed 
-  by @{ML OuterParse.prop}. However, they can include an optional theorem name plus
+  Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a
+  list of introduction rules, that is propositions with theorem
+  annotations. The introduction rules are propositions parsed by @{ML
+  OuterParse.prop}. However, they can include an optional theorem name plus
   some attributes. For example
 
 @{ML_response [display,gray] "let 
@@ -729,8 +725,8 @@
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
  
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
-  @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
-  attributes. The name has to end with @{text [quotes] ":"}---see argument of 
+  @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name 
+  has to end with @{text [quotes] ":"}---see the argument of 
   @{ML SpecParse.opt_thm_name} in Line 9.
 
   \begin{readmore}