--- a/CookBook/FirstSteps.thy	Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/FirstSteps.thy	Mon Jan 12 16:03:05 2009 +0000
@@ -294,8 +294,9 @@
       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  As can be seen, in the first case the arguments are correctly used, while in the 
-  second the @{term "P"} and @{text "Q"} from the antiquotation.
+  As can be seen, in the first case the arguments are correctly used, while the 
+  second generates a term involving the @{term "P"} and @{text "Q"} from the 
+  antiquotation.
 
   One tricky point in constructing terms by hand is to obtain the 
   fully qualified name for constants. For example the names for @{text "zero"} and

--- a/CookBook/Intro.thy	Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/Intro.thy	Mon Jan 12 16:03:05 2009 +0000
@@ -7,10 +7,13 @@
 chapter {* Introduction *}
 
 text {*
-  The purpose of this Cookbook is to guide the reader through the
-  first steps of Isabelle programming, and to provide recipes for
-  solving common problems. The code provided in the Cookbook is 
-  as far as possible checked against recent versions of Isabelle.
+  The purpose of this Cookbook is to guide the reader through the first steps
+  of Isabelle programming, and to explain some tricks of the trade. The code
+  provided in the Cookbook is as far as possible checked against recent
+  versions of Isabelle.  If something does not work, then please let us
+  know. If you have comments or like to add to the Cookbook, you are very
+  welcome.
+
 *}
 
 section {* Intended Audience and Prior Knowledge *}

--- a/CookBook/Parsing.thy	Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Jan 12 16:03:05 2009 +0000
@@ -553,19 +553,17 @@
 
 ML {* OuterSyntax.command *}
 
-section {* New Commands and Keyword Files *}
+section {* New Commands and Creating Keyword Files *}
 
 text {*
-
   Often new commands, for example for providing a new definitional principle,
-  need to be programmed. While this is not too difficult to do on the
-  ML-level, new commands, in order to be useful, need to be recognised by
+  need to be programmed. While this is not difficult to do on the ML-level,
+  new commands, in order to be useful, need to be recognised by
   ProofGeneral. This results in some subtle configuration issues, which we
   will explain in this section.
 
-
-  Let us start with a silly command, named \isacommand{foo}, which does nothing at all. 
-  It can be defined as
+  Let us start with a ``silly'' command, below named \isacommand{foo}, which does nothing at all. 
+  On the ML-level it can be defined as
 
 @{ML [display]
 "let
@@ -575,27 +573,53 @@
   OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
 end"}
 
-  The crucial function that makes the command \isacommand{foo} known to
-  Isabelle is @{ML OuterSyntax.command}.  It expects a name of a command, a
-  short description, a flag (we will explain it later more thoroughly) and a
+  The function @{ML OuterSyntax.command} expects a name for the command, a
+  short description, a flag (which we will explain it later on more thoroughly) and a
   parser for a top-level transition function (its purpose will also explained
-  later on). Lets also assume we packaged this function into a separate
-  theory named @{text "Command"}, say, and a file named @{text "Command.thy"}. 
+  later). 
 
-  We now need a keyword file, that can be loaded by ProofGeneral in
-  order to recognise \isacommand{foo} as command. Such a keyword file
-  can be generated with the command-line
+  While this is everything we have to do on the ML-level, we need 
+  now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral 
+  to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with 
+  the command-line
 
-  @{text [display] "$ isabelle keywords -k foo some-log-files"}
+  @{text [display] "$ isabelle keywords -k foo <some-log-files>"}
 
   The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
-  the case above the generated file is named @{text "isar-keywords-foo.el"}. This command
-  requires log files to be present (in order to extract the keywords from them). For 
+  the case above the generated file will be named @{text "isar-keywords-foo.el"}. 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 @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. 
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{figure}[t]
+  \begin{boxedminipage}{\textwidth}
+  \isacommand{theory}~@{text Command}\\
+  \isacommand{imports}~@{text Main}\\
+  \isacommand{begin}\\
+  \isacommand{ML}~\isa{\isacharverbatimopen}\\
+  @{ML
+"let
+  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
+  val flag = OuterKeyword.thy_decl
+in
+  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
+end"}\\
+  \isa{\isacharverbatimclose}\\
+  \isacommand{end}
+  \end{boxedminipage}
+  \caption{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{foo}.\label{fig:commandtheory}}
+  \end{figure}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+  For 
   our purposes it is sufficient to use the log files for the theories @{text "Pure"},
   @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
   containing the new command. @{text Pure} and @{text HOL} are usually compiled during the 
-  installation of Isabelle, if not this can be done conveniently using build script from 
-  the distribution
+  installation of Isabelle. So log files for them are already available. If not, then they 
+  can be conveniently compiled using build-script from the distribution
 
   @{text [display] 
 "$ ./build -m \"Pure\"
@@ -605,24 +629,41 @@
 
   @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
 
-  For the theory containing the new command \isacommand{foo}, we first
-  create a ``managed'' subdirectory by
+  For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 
+  with
+
+  @{text [display] "$ isabelle mkdir FooCommand"}
+
+  This creates a directory containing the files 
+
+  @{text [display] 
+"./IsaMakefile
+./FooCommand/ROOT.ML
+./FooCommand/document
+./FooCommand/document/root.tex"}
 
 
-  This creates files @{text "IsaMakefile"} and @{text "./FooCommand/ROOT.ML"}. We
-  need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
-  and add @{text "use_thy \"Command\";"} to @{text "./FooCommand/ROOT.ML"}.
-  Now we can compile the theory by just typing
+  We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
+  and add the line 
+
+  @{text [display] "use_thy \"Command\";"} 
+  
+  to the file @{text "./FooCommand/ROOT.ML"}. Now we can compile the theory by just typing
 
   @{text [display] "$ isabelle make"}
 
-  All these compilations created the log files that we are after. They are typically stored 
-  under the directory 
+  We created now the necessary log files. They are typically stored 
+  in the directory 
   
-  @{text [display]  "~/.isabelle/heaps/\<dots>\<dots>/\<dots>\<dots>/log"}
+  @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
 
-  where the dots stand for names of the current Isabelle distribution and 
-  hardware architecture. In it are the files
+  or something similar depending on your Isabelle distribution and architecture. 
+  Let us assume the name of this directory is stored in the shell variable 
+  @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing
+
+  @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
+ 
+  In this directory are the files
 
   @{text [display] 
 "Pure.gz
@@ -630,11 +671,6 @@
 Pure-ProofGeneral.gz
 HOL-FooCommand.gz"} 
 
-  Let us assume the directory with these files is stored in the shell variable 
-  @{text "ISABELLE_LOGS"}, by typing for example
-
-  @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
- 
   We can now create the keyword file with
 
 @{text [display]
@@ -642,12 +678,12 @@
        `$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral,HOL-FooCommand.gz}`"}
 
   The result is the file @{text "isar-keywords-foo.el"}, which needs to be 
-  copied in the directory @{text "~/.isabelle/etc"}. To make Isabelle use
-  this keyword file, we need to start it with the option @{text "-k foo"}:
+  copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
+  this keyword file, we need to start it with the option @{text "-k foo"}, i.e.
 
-  @{text [display] "isabelle -k foo a-theory-file"}
+  @{text [display] "isabelle -k foo <a-theory-file>"}
 
-  If we now run the original code creating the command
+  If we now run the original code
 
   @{ML [display]
 "let

--- a/CookBook/document/root.tex	Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/document/root.tex	Mon Jan 12 16:03:05 2009 +0000
@@ -11,6 +11,7 @@
 \usepackage{url}
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
 \usepackage{lineno}
+\usepackage{boxedminipage}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

Binary file cookbook.pdf has changed