--- a/CookBook/Parsing.thy	Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Feb 18 17:17:37 2009 +0000
@@ -528,7 +528,7 @@
 
 text {*
   There are a number of special purpose parsers that help with parsing
-  specifications for functions, inductive definitions and so on. In
+  specifications of functions, inductive definitions and so on. In
   Capter~\ref{chp:package}, for example, we will need to parse specifications
   for inductive predicates of the form:
 *}
@@ -555,13 +555,15 @@
     OuterParse.fixes -- 
     OuterParse.for_fixes --
     Scan.optional 
-        (OuterParse.$$$ "where" |--
-           OuterParse.!!! 
-             (OuterParse.enum1 "|" 
-                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+      (OuterParse.$$$ "where" |--
+         OuterParse.!!! 
+           (OuterParse.enum1 "|" 
+              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  To see what it returns, let us parse the string corresponding to the 
+  Note that the parser does not parse the ketword \simpleinductive. This 
+  will be done by the infrastructure that will eventually call this parser.
+  To see what the parser returns, let us parse the string corresponding to the 
   definition of @{term even} and @{term odd}:
 
 @{ML_response [display,gray]
@@ -581,7 +583,7 @@
       ((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 
-  optional locale; a list of variables with optional type-annotation and optional 
+  optional locale; a list of variables with optional type-annotation and  
   syntax-annotation; a list of for-fixes (fixed variables); and a list of rules 
   where each rule has optionally a name and an attribute.
 
@@ -591,10 +593,11 @@
 @{ML_response [display,gray]
 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
   
-  The function @{ML OuterParse.opt_target} returns @{ML NONE}, if no target is given.
+  returns the locale @{text [quotes] "test"}; if no target is given' like in  the
+  casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
 
   The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated 
-  list of variables that can include type annotations and syntax translations. 
+  list of variables that can include optional type annotations and syntax translations. 
   For example:\footnote{Note that in the code we need to write 
   @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
   in the compound type.}
@@ -613,7 +616,8 @@
 
 text {*
   Whenever types are given, they are stored in the @{ML SOME}s. Since types
-  are part of the inner syntax they are strings with some printing directives. 
+  are part of the inner syntax they are strings with some printing directives 
+  (see previous section). 
   If a syntax translation is present for a variable, then it is
   stored in the @{ML Mixfix} datastructure; no syntax translation is
   indicated by @{ML NoSyn}.
@@ -627,10 +631,10 @@
   but requires that this list is prefixed by the keyword \isacommand{for}.
 
 @{ML_response [display,gray]
-"parse OuterParse.for_fixes (filtered_input \"for foo and bar\")"
-"([(foo, NONE, NoSyn), (bar, NONE, NoSyn)],[])"}  
+"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 include the parser for a list of introduction rules, that is propositions 
+  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
   some attributes. For example
@@ -642,16 +646,20 @@
   (name, map Args.dest_src attrib)
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
  
+  A name of a theorem can be quite complicated, as it can include attrinutes.
   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. If you want to print out all currently known attributes a theorem 
   can have, you can use the function:
-*}
 
-ML{*Attrib.print_attributes @{theory}*}
+  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
+"COMP:  direct composition with rules (no lifting)
+HOL.dest:  declaration of Classical destruction rule
+HOL.elim:  declaration of Classical elimination rule 
+\<dots>"}
 
-text {*
-  For the inductive definitions described above only the attibutes @{text "[intro]"} and
+
+  For the inductive definitions described above only, the attibutes @{text "[intro]"} and
   @{text "[simp]"} make sense.
 
   \begin{readmore}