--- a/CookBook/Intro.thy	Wed Oct 29 13:58:36 2008 +0100
+++ b/CookBook/Intro.thy	Wed Oct 29 21:46:33 2008 +0100
@@ -33,13 +33,18 @@
 
   \begin{description}
   \item[The Implementation Manual] describes Isabelle
-  from a programmer's perspective, documenting both the underlying
+  from a high-level perspective, documenting both the underlying
   concepts and some of the interfaces. 
 
   \item[The Isabelle Reference Manual] is an older document that used
-  to be the main reference at a time when all proof scripts were written 
-  on the ML level. Many parts of this manual are outdated now, but some 
-  parts, particularly the chapters on tactics, are still useful.
+  to be the main reference of Isabelle at a time when all proof scripts 
+  were written on the ML level. Many parts of this manual are outdated 
+  now, but some  parts, particularly the chapters on tactics, are still 
+  useful.
+
+  \item[The Isar Reference Manual] is also an older document that provides
+  material about Isar and its implementation. Some material in it
+  is still useful.
   \end{description}
 
   Then of course there is:

--- a/CookBook/Parsing.thy	Wed Oct 29 13:58:36 2008 +0100
+++ b/CookBook/Parsing.thy	Wed Oct 29 21:46:33 2008 +0100
@@ -248,50 +248,92 @@
   Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings.
   This is because the parsers for the theory syntax, as well as the parsers for the 
   argument syntax of proof methods and attributes use the type 
-  @{ML_type OuterParse.token} (which is identical to the type @{ML_type OuterLex.token}).
+  @{ML_type OuterLex.token} (which is identical to the type @{ML_type OuterParse.token}).
 
   \begin{readmore}
   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"}.
   The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
   \end{readmore}
-*}
+
+  The structure @{ML_struct OuterLex} defines several kinds of token (for example 
+  @{ML "OuterLex.Ident"} for identifiers, @{ML "OuterLex.Keyword"} for keywords and
+  @{ML "OuterLex.Command"} for commands).
+  We can generate a token list using the function @{ML "OuterSyntax.scan"}, which we give
+  below @{ML "Position.none"} as argument since, at the moment, we are not interested in
+  generating precise error messages. The following\footnote{There is something funny 
+  going on with the pretty printing of the result token list.}
+
+@{ML_response [display] "OuterSyntax.scan Position.none \"hello world\"" 
+"[OuterLex.Token (\<dots>,(OuterLex.Ident, \"hello\"),\<dots>), 
+ OuterLex.Token (\<dots>,(OuterLex.Space, \" \"),\<dots>), 
+ OuterLex.Token (\<dots>,(OuterLex.Ident, \"world\"),\<dots>)]"}
+
+  produces three token where the first and the last are identifiers, since 
+  @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match 
+  any other category. The second indicates a space. If we parse
+
+@{ML_response [display] "OuterSyntax.scan Position.none \"inductive|for\"" 
+"[OuterLex.Token (\<dots>,(OuterLex.Command, \"inductive\"),\<dots>), 
+ OuterLex.Token (\<dots>,(OuterLex.Keyword, \"|\"),\<dots>), 
+ OuterLex.Token (\<dots>,(OuterLex.Keyword, \"for\"),\<dots>)]"}
+
+  we obtain a list of command/keyword token.
 
-ML {* 
-  let open OuterLex in 
-  OuterSyntax.scan Position.none "for" 
-  end;
+  Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
+ 
+@{ML_response [display]
+"let 
+  val input1 = OuterSyntax.scan Position.none \"where for\"
+  val input2 = OuterSyntax.scan Position.none \"|in\"
+in 
+  (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
+end"
+"((\"where\",\<dots>),(\"|\",\<dots>))"}
+
+  Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 
+  follows
+
+@{ML_response [display]
+"let 
+  val input = OuterSyntax.scan Position.none \"|in\"
+in 
+  (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
+end"
+"((\"|\",\"in\"),[])"}
+
+  The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty 
+  list of items recognized by the parser @{ML_text p}, where the items are 
+  separated by @{ML_text s}. For example
+
+@{ML_response [display]
+"let 
+  val input = OuterSyntax.scan Position.none \"in|in|in\\n\"
+in 
+  (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
+end" 
+"([\"in\",\"in\",\"in\"],[\<dots>])"}
+
+ @{ML_open "OuterParse.enum1"} works similarly, except that the list must be non-empty.
 
 *}
 
-ML {*
+text {* FIXME explain @{ML "OuterParse.!!!"} *}
+
+section {* Parsing Inner Syntax *}
 
-fun my_scan lex pos str =
-   Source.of_string str
-   |> Symbol.source {do_recover = false}
-   |> OuterLex.source {do_recover = SOME false}
-        (fn () => pairself (Scan.make_lexicon o map Symbol.explode) lex) pos
-   |> Source.exhaust;
+ML {*
+let 
+  val input = OuterSyntax.scan Position.none "0"
+in 
+  OuterParse.prop input
+end 
 
 *}
 
-ML {*
-let val toks = my_scan (["hello"], []) Position.none "hello foo bar"
-in (OuterParse.$$$ "hello") toks end
-*}
-
-ML {*
+text {* FIXME funny output for a proposition *}
 
-  let val input = [OuterLex.mk_text "hello", OuterLex.mk_text "world"];
-  in (Scan.one (fn _ => true)) input end
 
-*}
-
-text {*
-  explain @{ML "OuterParse.enum1"}, @{ML "OuterParse.prop"} 
-   @{ML "OuterParse.opt_target"}, @{ML "OuterParse.fixes"} 
-   @{ML "OuterParse.!!!"}, @{ML "OuterParse.for_fixes"} 
-*}
 
 chapter {* Parsing *}
 

--- a/CookBook/ROOT.ML	Wed Oct 29 13:58:36 2008 +0100
+++ b/CookBook/ROOT.ML	Wed Oct 29 21:46:33 2008 +0100
@@ -17,4 +17,5 @@
 use_thy "Recipes/Transformation";
 use_thy "Recipes/Antiquotes";
 
-use_thy "Solutions";
\ No newline at end of file
+use_thy "Solutions";
+use_thy "Readme";
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Readme.thy	Wed Oct 29 21:46:33 2008 +0100
@@ -0,0 +1,45 @@
+theory Readme
+imports Base
+begin
+
+chapter {* Comments for Authors of the Cookbook *}
+
+text {*
+
+  \begin{itemize}
+  \item You can make references to other Isabelle manuals using the 
+  reference names from those manuals. For this the following
+  four latex commands are defined:
+  
+  \begin{center}
+  \begin{tabular}{l|c|c}
+   & Chapters & Sections\\\hline
+  Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\
+  Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\
+  \end{tabular}
+  \end{center}
+
+  So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic 
+  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 
+  Isabelle code and also that responses of the ML-compiler can be shown.
+  For example
+
+  \begin{itemize}
+  \item[$\bullet$] @{text "@{ML \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"}
+  \end{itemize}
+
+  (FIXME: explain their usage)
+
+  \end{itemize}
+
+*}
+
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/document/isar-ref.aux	Wed Oct 29 21:46:33 2008 +0100
@@ -0,0 +1,332 @@
+\relax 
+\catcode 95\active
+\ifx\hyper@anchor\@undefined
+\global \let \oldcontentsline\contentsline
+\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
+\global \let \oldnewlabel\newlabel
+\gdef \newlabel#1#2{\newlabelxx{#1}#2}
+\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
+\AtEndDocument{\let \contentsline\oldcontentsline
+\let \newlabel\oldnewlabel}
+\else
+\global \let \hyper@last\relax 
+\fi
+
+\providecommand*\HyPL@Entry[1]{}
+\HyPL@Entry{0 << /S /D >> }
+\HyPL@Entry{1 << /S /r >> }
+\citation{isabelle-intro}
+\citation{isabelle-ref}
+\citation{proofgeneral}
+\citation{Aspinall:TACAS:2000}
+\citation{Wenzel:1999:TPHOL}
+\citation{Wenzel-PhD}
+\HyPL@Entry{5 << /S /D >> }
+\@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\@writefile{toc}{\contentsline {section}{\numberline {1.1}Overview}{1}{section.1.1}}
+\citation{Wenzel:2006:Festschrift}
+\citation{proofgeneral}
+\citation{Aspinall:TACAS:2000}
+\@writefile{toc}{\contentsline {section}{\numberline {1.2}User interfaces}{2}{section.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}Terminal sessions}{2}{subsection.1.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}Emacs Proof General}{2}{subsection.1.2.2}}
+\citation{proofgeneral}
+\citation{isabelle-sys}
+\citation{x-symbol}
+\@writefile{toc}{\contentsline {subsubsection}{Proof\nobreakspace  {}General as default Isabelle interface}{3}{section*.2}}
+\@writefile{toc}{\contentsline {subsubsection}{The X-Symbol package}{4}{section*.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {1.3}Isabelle/Isar theories}{4}{section.1.3}}
+\citation{Wenzel:1999:TPHOL}
+\citation{Wiedijk:2000:MV}
+\citation{Bauer-Wenzel:2000:HB}
+\citation{Bauer-Wenzel:2001}
+\citation{Wenzel-PhD}
+\newlabel{sec:isar-howto}{{1.4}{5}{How to write Isar proofs anyway? \label {sec:isar-howto}\relax }{section.1.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {1.4}How to write Isar proofs anyway? }{5}{section.1.4}}
+\citation{isabelle-sys}
+\citation{proofgeneral}
+\@writefile{toc}{\contentsline {chapter}{\numberline {2}Outer syntax}{6}{chapter.2}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\citation{isabelle-ref}
+\newlabel{sec:lex-syntax}{{2.1}{7}{Lexical matters \label {sec:lex-syntax}\relax }{section.2.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.1}Lexical matters }{7}{section.2.1}}
+\citation{isabelle-sys}
+\@writefile{toc}{\contentsline {section}{\numberline {2.2}Common syntax entities}{8}{section.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}Names}{8}{subsection.2.2.1}}
+\newlabel{sec:comments}{{2.2.2}{9}{Comments \label {sec:comments}\relax }{subsection.2.2.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}Comments }{9}{subsection.2.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.3}Type classes, sorts and arities}{9}{subsection.2.2.3}}
+\newlabel{sec:types-terms}{{2.2.4}{10}{Types and terms \label {sec:types-terms}\relax }{subsection.2.2.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.4}Types and terms }{10}{subsection.2.2.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.5}Mixfix annotations}{11}{subsection.2.2.5}}
+\citation{isabelle-ref}
+\newlabel{sec:syn-meth}{{2.2.6}{12}{Proof methods \label {sec:syn-meth}\relax }{subsection.2.2.6}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.6}Proof methods }{12}{subsection.2.2.6}}
+\newlabel{sec:syn-att}{{2.2.7}{14}{Attributes and theorems \label {sec:syn-att}\relax }{subsection.2.2.7}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.7}Attributes and theorems }{14}{subsection.2.2.7}}
+\newlabel{sec:term-decls}{{2.2.8}{16}{Term patterns and declarations \label {sec:term-decls}\relax }{subsection.2.2.8}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.8}Term patterns and declarations }{16}{subsection.2.2.8}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {3}Theory specifications}{18}{chapter.3}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{sec:begin-thy}{{3.1}{18}{Defining theories \label {sec:begin-thy}\relax }{section.3.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.1}Defining theories }{18}{section.3.1}}
+\newlabel{sec:target}{{3.2}{19}{Local theory targets \label {sec:target}\relax }{section.3.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.2}Local theory targets }{19}{section.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.3}Basic specification elements}{20}{section.3.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.4}Generic declarations}{22}{section.3.4}}
+\newlabel{sec:locale}{{3.5}{23}{Locales \label {sec:locale}\relax }{section.3.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.5}Locales }{23}{section.3.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.5.1}Locale specifications}{23}{subsection.3.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.5.2}Interpretation of locales}{27}{subsection.3.5.2}}
+\citation{Wenzel:1997:TPHOL}
+\citation{isabelle-classes}
+\newlabel{sec:class}{{3.6}{30}{Classes \label {sec:class}\relax }{section.3.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.6}Classes }{30}{section.3.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.6.1}The class target}{33}{subsection.3.6.1}}
+\newlabel{sec:axclass}{{3.6.2}{33}{Old-style axiomatic type classes \label {sec:axclass}\relax }{subsection.3.6.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.6.2}Old-style axiomatic type classes }{33}{subsection.3.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.7}Unrestricted overloading}{34}{section.3.7}}
+\newlabel{sec:ML}{{3.8}{35}{Incorporating ML code \label {sec:ML}\relax }{section.3.8}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.8}Incorporating ML code }{35}{section.3.8}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.9}Primitive specification elements}{36}{section.3.9}}
+\newlabel{sec:classes}{{3.9.1}{36}{Type classes and sorts \label {sec:classes}\relax }{subsection.3.9.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.9.1}Type classes and sorts }{36}{subsection.3.9.1}}
+\citation{isabelle-sys}
+\newlabel{sec:types-pure}{{3.9.2}{37}{Types and type abbreviations \label {sec:types-pure}\relax }{subsection.3.9.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.9.2}Types and type abbreviations }{37}{subsection.3.9.2}}
+\newlabel{sec:consts}{{3.9.3}{38}{Constants and definitions \label {sec:consts}\relax }{subsection.3.9.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.9.3}Constants and definitions }{38}{subsection.3.9.3}}
+\newlabel{sec:axms-thms}{{3.10}{41}{Axioms and theorems \label {sec:axms-thms}\relax }{section.3.10}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.10}Axioms and theorems }{41}{section.3.10}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.11}Oracles}{42}{section.3.11}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.12}Name spaces}{42}{section.3.12}}
+\newlabel{sec:syn-trans}{{3.13}{43}{Syntax and translations \label {sec:syn-trans}\relax }{section.3.13}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.13}Syntax and translations }{43}{section.3.13}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.14}Syntax translation functions}{44}{section.3.14}}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {chapter}{\numberline {4}Proofs}{46}{chapter.4}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{sec:proof-context}{{4.1}{46}{Context elements \label {sec:proof-context}\relax }{section.4.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.1}Context elements }{46}{section.4.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.2}Facts and forward chaining}{48}{section.4.2}}
+\newlabel{sec:goals}{{4.3}{50}{Goal statements \label {sec:goals}\relax }{section.4.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}Goal statements }{50}{section.4.3}}
+\newlabel{sec:proof-steps}{{4.4}{53}{Initial and terminal proof steps \label {sec:proof-steps}\relax }{section.4.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.4}Initial and terminal proof steps }{53}{section.4.4}}
+\newlabel{sec:pure-meth-att}{{4.5}{55}{Fundamental methods and attributes \label {sec:pure-meth-att}\relax }{section.4.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.5}Fundamental methods and attributes }{55}{section.4.5}}
+\newlabel{sec:term-abbrev}{{4.6}{58}{Term abbreviations \label {sec:term-abbrev}\relax }{section.4.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.6}Term abbreviations }{58}{section.4.6}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.7}Block structure}{59}{section.4.7}}
+\newlabel{sec:tactic-commands}{{4.8}{60}{Emulating tactic scripts \label {sec:tactic-commands}\relax }{section.4.8}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.8}Emulating tactic scripts }{60}{section.4.8}}
+\citation{isabelle-sys}
+\@writefile{toc}{\contentsline {section}{\numberline {4.9}Omitting proofs}{61}{section.4.9}}
+\newlabel{sec:obtain}{{4.10}{62}{Generalized elimination \label {sec:obtain}\relax }{section.4.10}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.10}Generalized elimination }{62}{section.4.10}}
+\newlabel{sec:calculation}{{4.11}{64}{Calculational reasoning \label {sec:calculation}\relax }{section.4.11}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.11}Calculational reasoning }{64}{section.4.11}}
+\newlabel{sec:cases-induct}{{4.12}{66}{Proof by cases and induction \label {sec:cases-induct}\relax }{section.4.12}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.12}Proof by cases and induction }{66}{section.4.12}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.12.1}Rule contexts}{66}{subsection.4.12.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.12.2}Proof methods}{68}{subsection.4.12.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.12.3}Declaring rules}{72}{subsection.4.12.3}}
+\citation{isabelle-sys}
+\citation{isabelle-sys}
+\citation{isabelle-hol-book}
+\@writefile{toc}{\contentsline {chapter}{\numberline {5}Document preparation }{74}{chapter.5}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:document-prep}{{5}{74}{Document preparation \label {ch:document-prep}\relax }{chapter.5}{}}
+\citation{isabelle-sys}
+\newlabel{sec:markup}{{5.1}{75}{Markup commands \label {sec:markup}\relax }{section.5.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.1}Markup commands }{75}{section.5.1}}
+\newlabel{sec:antiq}{{5.2}{77}{Antiquotations \label {sec:antiq}\relax }{section.5.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.2}Antiquotations }{77}{section.5.2}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-sys}
+\newlabel{sec:tags}{{5.3}{82}{Tagged commands \label {sec:tags}\relax }{section.5.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.3}Tagged commands }{82}{section.5.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.4}Draft presentation}{82}{section.5.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {6}Other commands }{84}{chapter.6}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:pure-syntax}{{6}{84}{Other commands \label {ch:pure-syntax}\relax }{chapter.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Diagnostics}{84}{section.6.1}}
+\citation{isabelle-ref}
+\citation{isabelle-sys}
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Inspecting the context}{86}{section.6.2}}
+\citation{isabelle-ref}
+\citation{isabelle-sys}
+\citation{proofgeneral}
+\citation{Aspinall:TACAS:2000}
+\newlabel{sec:history}{{6.3}{88}{History commands \label {sec:history}\relax }{section.6.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}History commands }{88}{section.6.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.4}System commands}{89}{section.6.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {7}Generic tools and packages }{90}{chapter.7}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:gen-tools}{{7}{90}{Generic tools and packages \label {ch:gen-tools}\relax }{chapter.7}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.1}Configuration options}{90}{section.7.1}}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {section}{\numberline {7.2}Basic proof tools}{91}{section.7.2}}
+\newlabel{sec:misc-meth-att}{{7.2.1}{91}{Miscellaneous methods and attributes \label {sec:misc-meth-att}\relax }{subsection.7.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.1}Miscellaneous methods and attributes }{91}{subsection.7.2.1}}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.2}Low-level equational reasoning}{93}{subsection.7.2.2}}
+\newlabel{sec:tactics}{{7.2.3}{94}{Further tactic emulations \label {sec:tactics}\relax }{subsection.7.2.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.3}Further tactic emulations }{94}{subsection.7.2.3}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\newlabel{sec:simplifier}{{7.3}{97}{The Simplifier \label {sec:simplifier}\relax }{section.7.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.3}The Simplifier }{97}{section.7.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.1}Simplification methods}{97}{subsection.7.3.1}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}Declaring rules}{99}{subsection.7.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.3}Simplification procedures}{100}{subsection.7.3.3}}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.4}Forward simplification}{101}{subsection.7.3.4}}
+\newlabel{sec:classical}{{7.4}{101}{The Classical Reasoner \label {sec:classical}\relax }{section.7.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.4}The Classical Reasoner }{101}{section.7.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.1}Basic methods}{101}{subsection.7.4.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.2}Automated methods}{102}{subsection.7.4.2}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\newlabel{sec:clasimp}{{7.4.3}{103}{Combined automated methods \label {sec:clasimp}\relax }{subsection.7.4.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.3}Combined automated methods }{103}{subsection.7.4.3}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.4}Declaring rules}{105}{subsection.7.4.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.5}Classical operations}{106}{subsection.7.4.5}}
+\newlabel{sec:object-logic}{{7.5}{106}{Object-logic setup \label {sec:object-logic}\relax }{section.7.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.5}Object-logic setup }{106}{section.7.5}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {8}Isabelle/HOL }{108}{chapter.8}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:hol}{{8}{108}{Isabelle/HOL \label {ch:hol}\relax }{chapter.8}{}}
+\newlabel{sec:hol-typedef}{{8.1}{108}{Primitive types \label {sec:hol-typedef}\relax }{section.8.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.1}Primitive types }{108}{section.8.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.2}Adhoc tuples}{109}{section.8.2}}
+\citation{NaraschewskiW-TPHOLs98}
+\newlabel{sec:hol-record}{{8.3}{110}{Records \label {sec:hol-record}\relax }{section.8.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.3}Records }{110}{section.8.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Basic concepts}{110}{subsection.8.3.1}}
+\citation{isabelle-hol-book}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Record specifications}{111}{subsection.8.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.3}Record operations}{112}{subsection.8.3.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.4}Derived rules and proof tools}{113}{subsection.8.3.4}}
+\citation{isabelle-HOL}
+\newlabel{sec:hol-datatype}{{8.4}{114}{Datatypes \label {sec:hol-datatype}\relax }{section.8.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.4}Datatypes }{114}{section.8.4}}
+\newlabel{sec:recursion}{{8.5}{115}{Recursive functions \label {sec:recursion}\relax }{section.8.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.5}Recursive functions }{115}{section.8.5}}
+\citation{isabelle-HOL}
+\citation{isabelle-function}
+\citation{isabelle-function}
+\citation{isabelle-function}
+\citation{isabelle-function}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.5.1}Proof methods related to recursive definitions}{117}{subsection.8.5.1}}
+\citation{isabelle-HOL}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.5.2}Old-style recursive function definitions (TFL)}{118}{subsection.8.5.2}}
+\citation{paulson-CADE}
+\newlabel{sec:hol-inductive}{{8.6}{119}{Inductive and coinductive definitions \label {sec:hol-inductive}\relax }{section.8.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.6}Inductive and coinductive definitions }{119}{section.8.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.6.1}Derived rules}{121}{subsection.8.6.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.6.2}Monotonicity theorems}{121}{subsection.8.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.7}Arithmetic proof support}{122}{section.8.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.8}Invoking automated reasoning tools -- The Sledgehammer}{122}{section.8.8}}
+\newlabel{sec:hol-induct-tac}{{8.9}{124}{Unstructured cases analysis and induction \label {sec:hol-induct-tac}\relax }{section.8.9}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.9}Unstructured cases analysis and induction }{124}{section.8.9}}
+\citation{isabelle-HOL}
+\@writefile{toc}{\contentsline {section}{\numberline {8.10}Executable code}{125}{section.8.10}}
+\citation{SML}
+\citation{OCaml}
+\citation{haskell-revised-report}
+\citation{isabelle-codegen}
+\newlabel{sec:hol-specification}{{8.11}{133}{Definition by specification \label {sec:hol-specification}\relax }{section.8.11}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.11}Definition by specification }{133}{section.8.11}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {9}Isabelle/HOLCF }{135}{chapter.9}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:holcf}{{9}{135}{Isabelle/HOLCF \label {ch:holcf}\relax }{chapter.9}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.1}Mixfix syntax for continuous operations}{135}{section.9.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.2}Recursive domains}{135}{section.9.2}}
+\citation{MuellerNvOS99}
+\@writefile{toc}{\contentsline {chapter}{\numberline {10}Isabelle/ZF }{137}{chapter.10}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:zf}{{10}{137}{Isabelle/ZF \label {ch:zf}\relax }{chapter.10}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.1}Type checking}{137}{section.10.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.2}(Co)Inductive sets and datatypes}{137}{section.10.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.2.1}Set definitions}{137}{subsection.10.2.1}}
+\citation{isabelle-ZF}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.2.2}Primitive recursive functions}{139}{subsection.10.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.2.3}Cases and induction: emulating tactic scripts}{140}{subsection.10.2.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {A}Isabelle/Isar quick reference }{141}{appendix.A}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ap:refcard}{{A}{141}{Isabelle/Isar quick reference \label {ap:refcard}\relax }{appendix.A}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.1}Proof commands}{141}{section.A.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.1}Primitives and basic syntax}{141}{subsection.A.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.2}Abbreviations and synonyms}{142}{subsection.A.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.3}Derived elements}{142}{subsection.A.1.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.4}Diagnostic commands}{142}{subsection.A.1.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.2}Proof methods}{143}{section.A.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.3}Attributes}{144}{section.A.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.4}Rule declarations and methods}{144}{section.A.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.5}Emulating tactic scripts}{145}{section.A.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.5.1}Commands}{145}{subsection.A.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.5.2}Methods}{145}{subsection.A.5.2}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {B}ML tactic expressions}{146}{appendix.B}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\@writefile{toc}{\contentsline {section}{\numberline {B.1}Resolution tactics}{146}{section.B.1}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {section}{\numberline {B.2}Simplifier tactics}{147}{section.B.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.3}Classical Reasoner tactics}{147}{section.B.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.4}Miscellaneous tactics}{147}{section.B.4}}
+\citation{isabelle-ref}
+\citation{isabelle-ref}
+\bibstyle{plain}
+\bibdata{../manual}
+\@writefile{toc}{\contentsline {section}{\numberline {B.5}Tacticals}{148}{section.B.5}}
+\bibcite{proofgeneral}{1}
+\bibcite{Aspinall:TACAS:2000}{2}
+\bibcite{Bauer-Wenzel:2000:HB}{3}
+\bibcite{Bauer-Wenzel:2001}{4}
+\bibcite{isabelle-codegen}{5}
+\bibcite{isabelle-classes}{6}
+\bibcite{isabelle-function}{7}
+\bibcite{OCaml}{8}
+\bibcite{SML}{9}
+\bibcite{MuellerNvOS99}{10}
+\bibcite{NaraschewskiW-TPHOLs98}{11}
+\bibcite{isabelle-HOL}{12}
+\bibcite{isabelle-hol-book}{13}
+\bibcite{isabelle-intro}{14}
+\bibcite{isabelle-ref}{15}
+\bibcite{isabelle-ZF}{16}
+\bibcite{paulson-CADE}{17}
+\bibcite{haskell-revised-report}{18}
+\bibcite{x-symbol}{19}
+\bibcite{Wenzel:2006:Festschrift}{20}
+\bibcite{Wenzel:1997:TPHOL}{21}
+\bibcite{Wenzel:1999:TPHOL}{22}
+\bibcite{Wenzel-PhD}{23}
+\bibcite{isabelle-sys}{24}
+\bibcite{Wiedijk:2000:MV}{25}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/document/root.rao	Wed Oct 29 21:46:33 2008 +0100
@@ -0,0 +1,31 @@
+% This file was generated by 'rail' from 'CookBook/generated/root.rai'
+\rail@i {1}{ 'simple\protect \unhbox \voidb@x \kern .06em\vbox {\hrule width.3em}inductive' target? fixes ('for' fixes)? \\ ('where' (thmdecl? prop + '|'))? ; }
+\rail@o {1}{
+\rail@begin{7}{}
+\rail@term{simple\protect \unhbox \voidb@x \kern .06em\vbox {\hrule width.3em}inductive}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{target}[]
+\rail@endbar
+\rail@nont{fixes}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{for}[]
+\rail@nont{fixes}[]
+\rail@endbar
+\rail@cr{3}
+\rail@bar
+\rail@nextbar{4}
+\rail@term{where}[]
+\rail@plus
+\rail@bar
+\rail@nextbar{5}
+\rail@nont{thmdecl}[]
+\rail@endbar
+\rail@nont{prop}[]
+\rail@nextplus{6}
+\rail@cterm{|}[]
+\rail@endplus
+\rail@endbar
+\rail@end
+}

--- a/CookBook/document/root.tex	Wed Oct 29 13:58:36 2008 +0100
+++ b/CookBook/document/root.tex	Wed Oct 29 21:46:33 2008 +0100
@@ -16,6 +16,10 @@
 \newcommand{\impref}[1]{\ref{I-#1}}
 \newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]}
 \newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]}
+\externaldocument[R-]{isar-ref}
+\newcommand{\isarref}[1]{\ref{R-#1}}
+\newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
+\newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
 
 \usepackage{pdfsetup}
 

--- a/IsaMakefile	Wed Oct 29 13:58:36 2008 +0100
+++ b/IsaMakefile	Wed Oct 29 21:46:33 2008 +0100
@@ -15,6 +15,9 @@
 
 USEDIR = $(ISATOOL) usedir -v true -i true -D generated
 
+rail:
+	rail CookBook/generated/root
+	cp CookBook/generated/root.rao CookBook/document
 
 ## CookBook
 

Binary file cookbook.pdf has changed