--- a/CookBook/FirstSteps.thy	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 21:46:04 2009 +0000
@@ -157,10 +157,11 @@
   map #name (Net.entries rules)
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  In the second example, the function @{ML rep_ss in MetaSimplifier} returns a record
-  containing information about the simpset. The rules of a simpset are stored in a 
-  discrimination net (a datastructure for fast indexing). From this net we can extract 
-  the entries using the function @{ML Net.entries}.
+  The second example extracts the theorem names that are stored in a simpset.
+  For this the function @{ML rep_ss in MetaSimplifier} returns a record
+  containing information about the simpset. The rules of a simpset are stored
+  in a discrimination net (a datastructure for fast indexing). From this net
+  we can extract the entries using the function @{ML Net.entries}.
 
   While antiquotations have many applications, they were originally introduced to
   avoid explicit bindings for theorems such as
@@ -185,8 +186,9 @@
   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
   \mbox{@{text "@{term \<dots>}"}}. For example
 
-  @{ML_response [display] "@{term \"(a::nat) + b = c\"}" 
-                          "Const (\"op =\", \<dots>)  $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  @{ML_response [display] 
+    "@{term \"(a::nat) + b = c\"}" 
+    "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
   representation of this term. This internal representation corresponds to the 

--- a/CookBook/Package/Ind_Interface.thy	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Wed Jan 14 21:46:04 2009 +0000
@@ -301,7 +301,8 @@
 structure of the tokens used, the second part of the library consists of combinators
 for dealing with specific token types.
 The following is an excerpt from the signature of @{ML_struct Scan}:
-\begin{mytable}
+
+\begin{table}
 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\
 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\
 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\
@@ -311,7 +312,7 @@
 @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\
 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}
-\end{mytable}
+\end{table}
 Interestingly, the functions shown above are so generic that they do not
 even rely on the input and output of the parser being a list of tokens.
 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser
@@ -348,10 +349,12 @@
 from simpler parsers. In order for these combinators to be useful, we also need
 some basic parsers. As an example, we consider the following two parsers
 defined in @{ML_struct Scan}:
-\begin{mytable}
+
+\begin{table}
 @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\
 @{ML "$$ : string -> string list -> string * string list"}
-\end{mytable}
+\end{table}
+
 The parser @{ML "one pred" for pred in Scan} parses exactly one token that
 satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only
 accepts a token that equals the string \texttt{s}. Note that we can easily
@@ -371,7 +374,8 @@
 The parser functions for the theory syntax are contained in the structure
 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
 In our parser, we will use the following functions:
-\begin{mytable}
+
+\begin{table}
 @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\
 @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->
   'a list * token list" in OuterParse} \\
@@ -382,7 +386,8 @@
 @{ML "for_fixes: token list ->
   (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
-\end{mytable}
+\end{table}
+
 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are
 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from
 @{ML_struct Scan}.
@@ -400,10 +405,12 @@
 and @{ML for_fixes in OuterParse}, respectively.
 In addition, the following function from @{ML_struct SpecParse} for parsing
 an optional theorem name and attribute, followed by a delimiter, will be useful:
-\begin{mytable}
+
+\begin{table}
 @{ML "opt_thm_name:
   string -> token list -> Attrib.binding * token list" in SpecParse}
-\end{mytable}
+\end{table}
+
 We now have all the necessary tools to write the parser for our
 \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
 @{ML_chunk [display] syntax}

--- a/CookBook/document/root.tex	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/document/root.tex	Wed Jan 14 21:46:04 2009 +0000
@@ -21,7 +21,7 @@
 \renewcommand{\isastyle}{\small\tt\slshape}%
 \isadroptag{theory}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For cross references to the other manuals:
 \usepackage{xr}
 \externaldocument[I-]{implementation}
@@ -33,21 +33,18 @@
 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
-\parindent 0pt\parskip 0.6ex
+\parindent 0pt\parskip 0.7ex
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\hyphenation{Isabelle}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % to work around a problem with \isanewline
 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% FIXME: WHAT DOES THIS DO?
-\renewenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\small\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for exercises, comments and readmores
 \newtheorem{exercise}{Exercise}[section]
 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
@@ -58,17 +55,15 @@
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% FIXME: THIS SHOULD NOT BE USED ANYMORE
-% a table environment with proper indentation
-\newenvironment{mytable}
-{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}
-{\end{tabular}\end{trivlist}}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\hyphenation{Isabelle}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% this is to draw a gray box around code
+\makeatletter\newenvironment{graybox}{%
+  \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
+  \colorbox{gray!10}{\usebox{\@tempboxa}}
+}\makeatother
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this hack is for getting rid of the ML {* ... *} 
 % scaffolding around function definitions
 \newenvironment{vanishML}{%
@@ -76,31 +71,27 @@
 \renewcommand{\isacharverbatimopen}{}%
 \renewcommand{\isacharverbatimclose}{}}{}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\makeatletter\newenvironment{graybox}{%
-   \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
-   \colorbox{gray!5}{\usebox{\@tempboxa}}
-}\makeatother
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \isakeeptag{CookBookML}
 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for line numbers
 \isakeeptag{linenumbers}
 \renewcommand{\isataglinenumbers}
 {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 
 \title{\mbox{}\\[-10ex]
        \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
        The Isabelle Programmer's Cookbook (fragment)}
+
 \author{with contributions by:\\[2ex] 
         \begin{tabular}{r@{\hspace{1.8mm}}l}
         Stefan & Berghofer\\
@@ -108,8 +99,8 @@
         Jeremy & Dawson\\
         Alexander & Krauss\\ 
         \end{tabular}}
+
 \maketitle
-
 \tableofcontents
 
 % generated text of all theories

Binary file cookbook.pdf has changed