--- a/CookBook/Parsing.thy	Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Jan 26 12:29:43 2009 +0000
@@ -580,11 +580,10 @@
   recognise \isacommand{foobar} as a command. Such a keyword file can be
   generated with the command-line:
 
-
   @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 
   The option @{text "-k foobar"} indicates which postfix the name of the keyword file 
-  will be assigned. In the case above the generated file will be named @{text
+  will be assigned. In the case above the file will be named @{text
   "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
   present (in order to extract the keywords from them). To generate these log
   files, we first package the code above into a separate theory file named
@@ -608,7 +607,7 @@
 end"}\\
   \isa{\isacharverbatimclose}\\
   \isacommand{end}
-  \end{graybox}\\[-4mm]
+  \end{graybox}
   \caption{\small The file @{text "Command.thy"} is necessary for generating a log 
   file. This log file enables Isabelle to generate a keyword file containing 
   the command \isacommand{foobar}.\label{fig:commandtheory}}
@@ -681,15 +680,17 @@
 
 @{text [display]
 "$ isabelle keywords -k foobar 
-     $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
+   $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
-  The result is the file @{text "isar-keywords-foobar.el"}. It should contain the
-  string @{text "foobar"} twice (check for example that @{text "grep foobar
-  isar-keywords-foobar.el"} returns something non-empty).  This keyword file
-  needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
-  Isabelle aware of this keyword file, we have to start Isabelle with the option @{text
+  The result is the file @{text "isar-keywords-foobar.el"}. It should contain
+  the string @{text "foobar"} twice (to see whether things went wrong, check
+  that @{text "grep foobar"} on this file returns something
+  non-empty).  This keyword file needs to
+  be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
+  aware of this keyword file, we have to start Isabelle with the option @{text
   "-k foobar"}, i.e.
 
+
   @{text [display] "$ isabelle -k foobar a_theory_file"}
 
   If we now build a theory on top of @{text "Command.thy"}, 
@@ -779,7 +780,7 @@
   proof state:
  
   \begin{isabelle}
-  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
   @{text "goal (1 subgoal)"}\\
   @{text "1. True \<and> True"}
   \end{isabelle}
@@ -787,7 +788,7 @@
   and we can build the proof
 
   \begin{isabelle}
-  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
   \isacommand{apply}@{text "(rule conjI)"}\\
   \isacommand{apply}@{text "(rule TrueI)+"}\\
   \isacommand{done}
@@ -796,14 +797,13 @@
   
   (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
 
-  (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-
   (FIXME read a name and show how to store theorems)
 
   (FIXME possibly also read a locale)
 *}
 
 (*<*)
+
 chapter {* Parsing *}
 
 text {*
@@ -1472,5 +1472,4 @@
 
 *}
 (*>*)
-
 end
\ No newline at end of file