--- a/CookBook/Parsing.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -192,7 +192,7 @@
   see the error message properly, we need to prefix the parser with the function 
   @{ML "Scan.error"}. For example
 
-  @{ML_response_fake [display,gray] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
+  @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
                                "Exception Error \"foo\" raised"}
 
   This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 
@@ -557,8 +557,9 @@
   ProofGeneral. This results in some subtle configuration issues, which we
   will explain in this section.
 
-  Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows.
-  To keep things simple this command does nothing at all. On the ML-level it can be defined as
+  To keep things simple, let us start with a ``silly'' command that does nothing 
+  at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 
+  defined as
 *}
 
 ML{*let
@@ -569,22 +570,22 @@
 end *}
 
 text {*
-  The function @{ML OuterSyntax.command} expects a name for the command, a
+  The crucial function @{ML OuterSyntax.command} expects a name for the command, a
   short description, a kind indicator (which we will explain later on more thoroughly) and a
-  parser for a top-level transition function (its purpose will also explained
+  parser producing a top-level transition function (its purpose will also explained
   later). 
 
   While this is everything we have to do on the ML-level, we need a keyword
   file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
   recognise \isacommand{foobar} as a command. Such a keyword file can be
-  generated with the command-line
+  generated with the command-line:
 
 
-  @{text [display] "$ isabelle keywords -k foobar some-log-files"}
+  @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 
-  The option @{text "-k foobar"} indicates which postfix the keyword file will
-  obtain. In the case above the generated file will be named @{text
-  "isar-keywords-foobar.el"}. However, this command requires log files to be
+  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
+  "isar-keywords-foobar.el"}. As indicated, 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
@@ -617,10 +618,13 @@
   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
-  \isacommand{foobar}-command. @{text Pure} and @{text HOL} are usually
-  compiled during the installation of Isabelle. So log files for them should be
-  already available. If not, then they can be conveniently compiled using
-  build-script from the Isabelle distribution
+  \isacommand{foobar}-command. If you target another logics besides HOL, such
+  as Nominal or ZF, then you need to adapt the log files appropriately.
+  @{text Pure} and @{text HOL} are usually compiled during the installation of
+  Isabelle. So log files for them should be already available. If not, then
+  they can be conveniently compiled using build-script from the Isabelle
+  distribution
+
 
   @{text [display] 
 "$ ./build -m \"Pure\"
@@ -635,7 +639,7 @@
 
   @{text [display] "$ isabelle mkdir FoobarCommand"}
 
-  This creates a directory containing the files 
+  This generates a directory containing the files 
 
   @{text [display] 
 "./IsaMakefile
@@ -653,18 +657,17 @@
 
   @{text [display] "$ isabelle make"}
 
-  We created finally all the necessary log files. They are typically stored 
+  We created finally all the necessary log files. They are stored 
   in the directory 
   
   @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
 
-  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
+  or something similar depending on your Isabelle distribution and architecture.
+  One quick way to assign a shell variable to this directory is by typing
 
   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
  
-  on the Unix prompt. This directory should include the files
+  on the Unix prompt. The directory should include the files
 
   @{text [display] 
 "Pure.gz
@@ -672,21 +675,22 @@
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"} 
 
-  They are the ones we use for creating the keyword files. The corresponding  Unix command
-  is
+  They are the ones we need for creating the keyword files. Assuming the name 
+  of the directory is in  @{text "ISABELLE_LOGS"},
+  then the Unix command for creating the keyword file is:
 
 @{text [display]
 "$ isabelle keywords -k foobar 
      $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 [quotes] "grep foobar
+  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 use this keyword file, we have to start it with the option @{text
+  Isabelle aware of this keyword file, we have to start it with the option @{text
   "-k foobar"}, i.e.
 
-  @{text [display] "$ isabelle -k foobar a-theory-file"}
+  @{text [display] "$ isabelle -k foobar a_theory_file"}
 
   If we now run the original code
 *}
@@ -699,19 +703,17 @@
 end *}
 
 text {*
-  then we can make use of \isacommand{foobar}! Similarly with any other new command. 
+  then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}! 
+  Similarly with any other new command. 
 
-  In the example above, we built the theories on top of the HOL-logic. If you
-  target other logics, such as Nominal or ZF, then you need to adapt the
-  log files appropriately.
 
-  At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit 
+  At the moment \isacommand{foobar} is not very useful. Let us next refine it a bit 
   by taking a proposition as argument and printing this proposition inside
   the tracing buffer. 
 
   The crucial part of a command is the function that determines
-  the behaviour of the command. In the code above we used the the 
-  @{text do_nothing}-function, which because of @{ML Scan.succeed} does not parse 
+  the behaviour of the command. In the code above we used a
+  ``do-nothing''-function, which because of @{ML Scan.succeed} does not parse 
   any argument, but immediately returns the simple toplevel function 
   @{ML "Toplevel.theory I"}. We can replace this code by a function that first 
   parses a proposition (using the parser @{ML OuterParse.prop}), then prints out 
@@ -729,22 +731,25 @@
 text {*
   Now we can type for example
 
-  @{ML_response_fake_both [display,gray] "foobar \"True \<and> False\"" "True \<and> False"}
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  @{text "> True \<and> False"}
+  \end{isabelle}
   
   and see the proposition in the tracing buffer.  
 
-  Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator
+  Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator
   for the command.  This means that the command finishes as soon as the
   arguments are processed. Examples of this kind of commands are
-  \isacommand{definition} and \isacommand{declare}.  In other cases, however,
+  \isacommand{definition} and \isacommand{declare}.  In other cases
   commands are expected to parse some arguments, for example a proposition,
   and then ``open up'' a proof in order to prove the proposition (think of
   \isacommand{lemma}) or prove some other properties (for example in
-  \isacommand{function}). To achieve this behaviour we have to use the kind
+  \isacommand{function}). To achieve this behaviour, we have to use the kind
   indicator @{ML thy_goal in OuterKeyword}.
 
-  Below we change \isacommand{foobar} is such a way that an proposition as
-  argument and then start a proof in order to prove it. Therefore in Line 13
+  Below we change \isacommand{foobar} so that it expects a proposition as
+  argument and then starts a proof in order to prove it. Therefore in Line 13
   below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 
@@ -766,25 +771,30 @@
 end *}
 
 text {*
-  The function @{text set_up_thm} takes a string (the proposition) and a context.
-  The context is necessary in order to convert the string into a proper proposition
-  using the function @{ML Syntax.read_prop}. In Line 6 we use the function
-  @{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to
-  11 contain the parser for the proposition.
+  The function @{text set_up_thm} takes a string (the proposition to be
+  proved) and a context.  The context is necessary in order to be able to use
+  @{ML Syntax.read_prop}, which converts a string into a proper proposition.
+  In Line 6 the function @{ML Proof.theorem_i} starts the proof for the 
+  proposition. In Lines 9 to 11 contain the parser for the proposition.
 
-  If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 
+  If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following 
   proof state:
  
-  @{ML_response_fake_both [display,gray] "foobar \"True \<and> True\"" 
-"goal (1 subgoal):
-1. True \<and> True"}
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  @{text "goal (1 subgoal)"}\\
+  @{text "1. True \<and> True"}
+  \end{isabelle}
 
   and we can build the proof
 
-  @{text [display,gray] "foobar \"True \<and> True\"
-apply(rule conjI)
-apply(rule TrueI)+
-done"} 
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  \isacommand{apply}@{text "(rule conjI)"}\\
+  \isacommand{apply}@{text "(rule TrueI)+"}\\
+  \isacommand{done}
+  \end{isabelle}
+
   
   (FIXME What does @{text "Toplevel.theory"}?)
 

--- a/CookBook/Recipes/Antiquotes.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -15,18 +15,21 @@
   Document antiquotations can be used for ensuring consistent type-setting of
   various entities in a document. They can also be used for sophisticated
   \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you
-  obtain a list of all available document antiquotations and their options.
+  obtain a list of all currently available document antiquotations and their options.
 
   Below we give the code for two additional antiquotations that can be used to typeset
   ML-code and also to check whether the given code actually compiles. This
   provides a sanity check for the code and also allows one to keep documents
   in sync with other code, for example Isabelle.
 
-  We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This
-  antiquotation takes a piece of code as argument. The code is checked
-  by sending the ML-expression @{text [quotes] "val _ = \<dots>"} containing the
-  given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}
-  in Line 4 below). The complete code of the antiquotation is as follows:
+  We first describe the antiquotation @{text "ML_checked"} with the syntax:
+ 
+  @{text [display] "@{ML_checked \"a_piece_of_code\"}"}
+
+  The code is checked by sending the ML-expression @{text [quotes] "val _ =
+  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
+  "ML_Context.eval_in"} in Line 4 below). The complete code of the
+  antiquotation is as follows:
 
 *}
 
@@ -44,16 +47,16 @@
 
   Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
   in this case the code given as argument. As mentioned before, this argument 
-  is send to the ML-compiler in the line 4 using the function @{ML ml_val},
-  which constructs an apropriate ML-expression.
+  is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
+  which constructs the appropriate ML-expression.
   If the code is ``approved'' by the compiler, then the output function @{ML
   "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the
   code. This function expects that the code is a list of strings where each
   string correspond to a line in the output. Therefore the use of 
   @{ML "(space_explode \"\\n\" txt)" for txt} 
   which produces this list according to linebreaks.  There are a number of options for antiquotations
-  that are observed by @{ML ThyOutput.output_list} when printing the code (for
-  example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
+  that are observed by @{ML ThyOutput.output_list} when printing the code (including
+  @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
 
   \begin{readmore}
   For more information about options of antiquotations see \rsccite{sec:antiq}).
@@ -62,7 +65,6 @@
   Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
   information about the line number, in case an error is detected. We 
   can improve the code above slightly by writing 
-
 *}
 
 ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) =
@@ -84,22 +86,24 @@
   somebody changes the definition of \mbox{@{ML "(op +)"}}.
 
 
-  The second antiquotation extends the first by allowing also to give
-  hints what the result of the ML-code should be and to check the consistency of 
-  the actual result with these hints. For this we are going to implement the 
-  antiquotation  
-  @{text "@{ML_resp \"expr\" \"pat\"}"}
-  whose first argument is the ML-code and the second is a pattern specifying
-  the result. To add some convenience and allow dealing with large outputs,
-  the user can give a partial specification including abbreviations 
-  @{text [quotes] "\<dots>"}.
+  The second antiquotation we describe extends the first by allowing also to give
+  a pattern that specifies what the result of the ML-code should be and to check 
+  the consistency of the actual result with the given pattern. For this we are going 
+  to implement the antiquotation  
+  
+  @{text [display] "@{ML_resp \"a_piece_of_code\" \"pattern\"}"}
+  
+  To add some convenience and also to deal with large outputs,
+  the user can give a partial specification by giving the abbreviation 
+  @{text [quotes] "\<dots>"}. For example @{text "(\<dots>,\<dots>)"} for a pair.
 
-  Whereas in the antiquotation @{text "@{ML_checked \"expr\"}"} above, we have
-  sent the expression 
-  @{text [quotes] "val _ = expr"} to the compiler, in this antiquotation the wildcard
-  @{text "_"} we will be replaced by a proper pattern constructed the hints. To
-  do this we need to replace the @{text [quotes] "\<dots>"} by @{text [quotes] "_"} 
-  before sending the code to the compiler. The following function will do this:
+  Whereas in the antiquotation @{text "@{ML_checked \"piece_of_code\"}"} above, 
+  we have sent the expression 
+  @{text [quotes] "val _ = piece_of_code"} to the compiler, in the second the 
+  wildcard @{text "_"} we will be replaced by a proper pattern. To do this we 
+  need to replace the @{text [quotes] "\<dots>"} by 
+  @{text [quotes] "_"}  before sending the code to the compiler. The following 
+  function will do this:
 
 *}
 
@@ -154,8 +158,8 @@
   @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} 
 
   In both cases, the check by the compiler ensures that code and result match. A limitation
-  of this antiquotation is that the hints can only be given for results that can actually
-  be constructed as a pattern. This excludes values that are abstract datatypes, like 
+  of this antiquotation, however, is that the hints can only be given in case
+  they can be constructed as a pattern. This excludes values that are abstract datatypes, like 
   theorems or cterms.
 
 *}

--- a/CookBook/Recipes/Config.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -12,7 +12,7 @@
 
   {\bf Solution:} This can be achieved using configuration values.\smallskip
 
-  Assume you want to control three values, say @{ML_text bval} containing a
+  Assume you want to control three values, namely @{ML_text bval} containing a
   boolean,  @{ML_text ival} containing an integer and @{ML_text sval} 
   containing a string. These values can be declared on the ML-level with
 *}
@@ -23,7 +23,7 @@
 
 text {* 
   where each value needs to be given a default. To enable these values, they need to 
-  be set up using 
+  be set up by  
 *}
 
 setup {* setup_bval *} 

--- a/CookBook/Recipes/NamedThms.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -48,9 +48,11 @@
 
 text {* and query the remaining ones with:
 
-@{ML_response_fake_both [display,gray] "thm foo" 
-"?C
-?B"}
+  \begin{isabelle}
+  \isacommand{thm}~@{text "foo"}\\
+  @{text "> ?C"}\\
+  @{text "> ?B"}\\
+  \end{isabelle}
 
   On the ML-level the rules marked with @{text "foo"} an be retrieved
   using the function @{ML FooRules.get}:

--- a/CookBook/document/root.tex	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/document/root.tex	Fri Jan 16 14:57:36 2009 +0000
@@ -60,7 +60,7 @@
 % this is to draw a gray box around code
 \makeatletter\newenvironment{graybox}{%
   \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}%
-  \colorbox{gray!10}{\usebox{\@tempboxa}}
+  \colorbox{gray!20}{\usebox{\@tempboxa}}
 }\makeatother
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Binary file cookbook.pdf has changed