--- a/CookBook/FirstSteps.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/FirstSteps.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -79,8 +79,8 @@
   However this only works if the type of what is converted is monomorphic and is not 
   a function.
 
-  The funtion @{ML "warning"} should only be used for testing purposes, because any
-  output this funtion generates will be overwritten as soon as an error is
+  The function @{ML "warning"} should only be used for testing purposes, because any
+  output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
   function @{ML tracing} should be used. This function writes all output into
   a separate tracing buffer. For example
@@ -89,7 +89,7 @@
 
   It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
-  amounts of trace output. This rediretion can be achieved using the code
+  amounts of trace output. This redirection can be achieved using the code
 *}
 
 ML{* 
@@ -214,7 +214,7 @@
 
   Hint: The third term is already quite big, and the pretty printer
   may omit parts of it by default. If you want to see all of it, you
-  can use the following ML funtion to set the limit to a value high 
+  can use the following ML function to set the limit to a value high 
   enough:
   \end{exercise}
 
@@ -253,7 +253,7 @@
   While antiquotations are very convenient for constructing terms and types, 
   they can only construct fixed terms. Unfortunately, one often needs to construct terms
   dynamically. For example, a function that returns the implication 
-  @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
+  @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
   as arguments can only be written as
 *}
 
@@ -292,7 +292,7 @@
   The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
-  Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
+  Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   expansion automatically, for example:
 
   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}

--- a/CookBook/Intro.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/Intro.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -58,7 +58,7 @@
   \end{description}
 
   The Cookbook is written in such a way that the code examples in it are 
-  synchronised with fairly recent versions of the code.
+  checked against recent versions of the code.
 
 *}
 

--- a/CookBook/Parsing.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/Parsing.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -45,7 +45,7 @@
   @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
   @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
 
-  This function will either succeed (as in the two examples above) or raise the exeption 
+  This function will either succeed (as in the two examples above) or raise the exception 
   @{ML_text "FAIL"} if no string can be consumed. For example trying to parse
 
   @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" 
@@ -68,7 +68,7 @@
   
   Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
   Scan.one}, in that it takes a predicate as argument and then parses exactly
-  one item from the input list satisfying this prediate. For example the
+  one item from the input list satisfying this predicate. For example the
   following parser either consumes an @{ML_text [quotes] "h"} or a @{ML_text
   [quotes] "w"}:
 
@@ -83,7 +83,7 @@
 end"
     "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  Two parser can be connected in sequence by using the funtion @{ML "(op --)"}. 
+  Two parser can be connected in sequence by using the function @{ML "(op --)"}. 
   For example parsing @{ML_text "h"}, @{ML_text "e"} and @{ML_text "l"} in this 
   sequence can be achieved by
 
@@ -107,7 +107,7 @@
 end"
   "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing funtion 
+  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 
   for parsers, except that they discard the item being parsed by the first (respectively second)
   parser. For example
   
@@ -161,11 +161,11 @@
   which @{ML_text p} 
   is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail 
   and the 
-  alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong
+  alternative parser @{ML_text r} will be tried. However in many circumstance this will be the wrong
   parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then 
   caused by the
-  failure of @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation
-  can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of
+  failure of @{ML_text r}, not by the absence of @{ML_text q} in the input. This kind of situation
+  can be avoided by using the function @{ML "(op !!)"}. This function aborts the whole process of
   parsing in case of a failure and invokes an error message. For example if we invoke the parser
   
   @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
@@ -333,7 +333,7 @@
  Token (\<dots>,(Keyword, \"|\"),\<dots>), 
  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 
-  we obtain a list consiting of only a command and two keyword tokens.
+  we obtain a list consisting of only a command and two keyword tokens.
   If you want to see which keywords and commands are currently known, use
   the following (you might have to adjust the @{ML print_depth} in order to
   see the complete list):

--- a/CookBook/Readme.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/Readme.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -23,17 +23,24 @@
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for the 
-  cookbook so that written text can be kept in sync with the 
+  cookbook. This allows to check the written text against the current
   Isabelle code and also that responses of the ML-compiler can be shown.
-  The are:
+  Therefore authors are strongly encouraged to use antiquotations wherever
+  it is appropriate.
+  
+  The following antiquotations are in use:
 
   \begin{itemize}
-  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value computations. It checks whether
-  the ML-expression is valid ML-code, but only works for closed expression.
-  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text ML}-antiquotation except, 
-  that  it can also deal with open expressions and expressions that need to be evaluated inside structures. 
-  The free variables or structures need to be listed after the @{ML_text "for"}. For example 
+  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value
+  computations. It checks whether the ML-expression is valid ML-code, but only
+  works for closed expression.
+
+  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text
+  ML}-antiquotation except, that it can also deal with open expressions and
+  expressions that need to be evaluated inside structures. The free variables
+  or structures need to be listed after the @{ML_text "for"}. For example
   @{text "@{ML_open \"a + b\" for a b}"}.
+
   \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first
   expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the
   second is a pattern that specifies the result the first expression
@@ -44,17 +51,22 @@
   constructed. It does not work when the code produces an exception or is an
   abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
-  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like the 
-  @{ML_text ML_response}-anti\-quotation, except that the result-specification is not
-  checked.
-  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when referring to a file. 
-  It checks whether the file exists.
+  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like
+  the @{ML_text ML_response}-anti\-quotation, except that the
+  result-specification is not checked.
+
+  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when
+  referring to a file. It checks whether the file exists.  
   \end{itemize}
 
+
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
   environments. Some \LaTeX-hack, however, does not print the environment markers.
 
+  \item Line numbers for code can be shown using 
+  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.
+
   \end{itemize}
 
 *}

Binary file cookbook.pdf has changed