--- a/CookBook/FirstSteps.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/FirstSteps.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -75,7 +75,7 @@
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, for example:
 
-  @{ML_response_fake [display] "warning (makestring 1)" "1"} 
+  @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} 
 
   However this only works if the type of what is converted is monomorphic and is not 
   a function.
@@ -157,7 +157,7 @@
   @{ML_response_fake [display] "@{simpset}" "\<dots>"}
 
   (FIXME: what does a simpset look like? It seems to be the same problem
-  like tokens.)
+  as with tokens.)
 
   While antiquotations nowadays have many applications, they were originally introduced to 
   avoid explicit bindings for theorems such as

--- a/CookBook/Intro.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Intro.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -9,13 +9,13 @@
   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 
-  checked against recent versions of Isabelle.
+  as far as possible checked against recent versions of Isabelle.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
 
 text {* 
-  This cookbook targets an audience who already knows how to use Isabelle
+  This Cookbook targets an audience who already knows how to use Isabelle
   for writing theories and proofs. We also assume that readers are 
   familiar with the functional programming language ML, the language in 
   which most of Isabelle is implemented. If you are unfamiliar with either of

--- a/CookBook/Package/Ind_Interface.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -434,14 +434,21 @@
   (local_theory -> local_theory) ->
   Toplevel.transition -> Toplevel.transition"}
 which, apart from the local theory transformer, takes an optional name of a locale
-to be used as a basis for the local theory. The whole parser for our command has type
-@{ML_type [display] "OuterLex.token list ->
+to be used as a basis for the local theory. 
+
+(FIXME : needs to be adjusted to new parser type)
+
+{\it
+The whole parser for our command has type
+@{ML_text [display] "OuterLex.token list ->
   (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"}
-which is abbreviated by @{ML_type OuterSyntax.parser_fn}. The new command can be added
+which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added
 to the system via the function
-@{ML [display] "OuterSyntax.command :
+@{ML_text [display] "OuterSyntax.command :
   string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"}
-which imperatively updates the parser table behind the scenes. In addition to the parser, this
+which imperatively updates the parser table behind the scenes. }
+
+In addition to the parser, this
 function takes two strings representing the name of the command and a short description,
 as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of
 command we intend to add. Since we want to add a command for declaring new concepts,

--- a/CookBook/Parsing.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Parsing.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -59,7 +59,7 @@
   might be explored. 
   \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
   in @{text "($$ \"h\") []"}.
-  \item @{text "ABORT"} is the exception which is raised when a dead end is reached. 
+  \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
   It is used for example in the function @{ML "(op !!)"} (see below).
   \end{itemize}
 
@@ -93,7 +93,7 @@
   Note how the result of consumed strings builds up on the left as nested pairs.  
 
   If, as in the previous example, one wants to parse a particular string, 
-  then one should rather use the function @{ML Scan.this_string}:
+  then one should use the function @{ML Scan.this_string}:
 
   @{ML_response [display] "Scan.this_string \"hel\" (explode \"hello\")"
                           "(\"hel\", [\"l\", \"o\"])"}
@@ -263,7 +263,7 @@
   end of the input string.
 
   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 
-  parse the input then the whole parser fails; if not, then the second is tried. Therefore
+  parse the input, then the whole parser fails; if not, then the second is tried. Therefore
   
   @{ML_response_fake_both [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
                                "Exception FAIL raised"}
@@ -277,7 +277,7 @@
 
   The functions @{ML Scan.repeat} and @{ML Scan.unless} can be combined to read any
   input until a certain marker symbol is reached. In the example below the marker
-  symbol is a @{text [quotes] "*"} which causes the parser to stop:
+  symbol is a @{text [quotes] "*"}.
 
   @{ML_response [display]
 "let 
@@ -315,7 +315,7 @@
 end" 
 "(\"foo bar foo\",[])"}
 
-  where the single strings in the parsed output are transformed
+  where the single-character strings in the parsed output are transformed
   back into one string.
  
   \begin{exercise}\label{ex:scancmts}

--- a/CookBook/Readme.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Readme.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -7,14 +7,14 @@
 text {*
 
   \begin{itemize}
-  \item The cookbook can be compiled on the command-line with:
+  \item The Cookbook can be compiled on the command-line with:
 
   \begin{center}
   @{text "isabelle make"}
   \end{center}
 
   You very likely need a recent snapshot of Isabelle in order to compile
-  the cookbook.
+  the Cookbook.
 
   \item You can include references to other Isabelle manuals using the 
   reference names from those manuals. To do this the following
@@ -32,7 +32,7 @@
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for the 
-  cookbook. They allow to check the written text against the current
+  Cookbook. They allow to check the written text against the current
   Isabelle code and also allow to show responses of the ML-compiler.
   Therefore authors are strongly encouraged to use antiquotations wherever
   appropriate.

--- a/IsaMakefile	Wed Dec 17 05:08:33 2008 +0000
+++ b/IsaMakefile	Sat Jan 03 20:44:54 2009 +0000
@@ -13,7 +13,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i true -D generated
+USEDIR = $(ISATOOL) usedir -v true -D generated
 
 rail:
 	rail CookBook/generated/root

Binary file cookbook.pdf has changed