isabelle-cookbook: changeset 300:f286dfa9f173

--- a/ProgTutorial/document/implementation.aux	Sun Aug 02 08:44:41 2009 +0200
+++ b/ProgTutorial/document/implementation.aux	Mon Aug 03 13:53:04 2009 +0200
@@ -75,81 +75,91 @@
 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Auxiliary definitions}{24}{subsection.2.3.2}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Definitions of auxiliary connectives}}{24}{figure.2.5}}
 \newlabel{fig:pure-aux}{{2.5}{24}{Definitions of auxiliary connectives\relax }{figure.2.5}{}}
+\citation{Gentzen:1935}
+\citation{extensions91}
 \newlabel{sec:obj-rules}{{2.4}{25}{Object-level rules \label {sec:obj-rules}\relax }{section.2.4}{}}
 \@writefile{toc}{\contentsline {section}{\numberline {2.4}Object-level rules }{25}{section.2.4}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{26}{chapter.3}}
-\@writefile{lof}{\addvspace {10\p@ }}
-\@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:tactical-goals}{{3.1}{26}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{26}{section.3.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{27}{section.3.2}}
-\newlabel{sec:resolve-assume-tac}{{3.2.1}{29}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{29}{subsection.3.2.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{31}{subsection.3.2.2}}
-\newlabel{sec:tacticals}{{3.3}{32}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{32}{section.3.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{33}{chapter.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.1}Hereditary Harrop Formulae}{25}{subsection.2.4.1}}
+\citation{Miller:1991}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.2}Rule composition}{27}{subsection.2.4.2}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{29}{chapter.3}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:variables}{{4.1}{33}{Variables \label {sec:variables}\relax }{section.4.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{33}{section.4.1}}
-\newlabel{sec:assumptions}{{4.2}{35}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{35}{section.4.2}}
-\citation{isabelle-isar-ref}
-\newlabel{sec:results}{{4.3}{37}{Results \label {sec:results}\relax }{section.4.3}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{37}{section.4.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {5}Isar proof texts}{39}{chapter.5}}
+\newlabel{sec:tactical-goals}{{3.1}{29}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{29}{section.3.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{30}{section.3.2}}
+\newlabel{sec:resolve-assume-tac}{{3.2.1}{32}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{32}{subsection.3.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{34}{subsection.3.2.2}}
+\newlabel{sec:tacticals}{{3.3}{35}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{35}{section.3.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{36}{chapter.4}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {5.1}Proof context}{39}{section.5.1}}
-\newlabel{sec:isar-proof-state}{{5.2}{39}{Proof state \label {sec:isar-proof-state}\relax }{section.5.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.2}Proof state }{39}{section.5.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.3}Proof methods}{39}{section.5.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.4}Attributes}{39}{section.5.4}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {6}Structured specifications}{40}{chapter.6}}
+\newlabel{sec:variables}{{4.1}{36}{Variables \label {sec:variables}\relax }{section.4.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{36}{section.4.1}}
+\newlabel{sec:assumptions}{{4.2}{38}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{38}{section.4.2}}
+\citation{isabelle-isar-ref}
+\newlabel{sec:results}{{4.3}{40}{Results \label {sec:results}\relax }{section.4.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{40}{section.4.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {5}Syntax and type-checking}{42}{chapter.5}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\@writefile{toc}{\contentsline {chapter}{\numberline {6}Isar language elements}{43}{chapter.6}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {6.1}Specification elements}{40}{section.6.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.2}Type-inference}{40}{section.6.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.3}Local theories}{40}{section.6.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {7}System integration}{41}{chapter.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Proof commands}{43}{section.6.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Proof methods}{43}{section.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}Attributes}{43}{section.6.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {7}Local theory specifications}{44}{chapter.7}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\@writefile{toc}{\contentsline {section}{\numberline {7.1}Definitional elements}{44}{section.7.1}}
+\citation{Haftmann-Wenzel:2009}
+\@writefile{toc}{\contentsline {section}{\numberline {7.2}Morphisms and declarations}{46}{section.7.2}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {8}System integration}{47}{chapter.8}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:isar-toplevel}{{7.1}{41}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.7.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.1}Isar toplevel }{41}{section.7.1}}
-\newlabel{sec:toplevel-transition}{{7.1.1}{42}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.7.1.1}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Toplevel transitions }{42}{subsection.7.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Toplevel control}{44}{subsection.7.1.2}}
-\newlabel{sec:ML-toplevel}{{7.2}{44}{ML toplevel \label {sec:ML-toplevel}\relax }{section.7.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.2}ML toplevel }{44}{section.7.2}}
-\newlabel{sec:theory-database}{{7.3}{46}{Theory database \label {sec:theory-database}\relax }{section.7.3}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.3}Theory database }{46}{section.7.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{49}{appendix.A}}
+\newlabel{sec:isar-toplevel}{{8.1}{47}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.8.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.1}Isar toplevel }{47}{section.8.1}}
+\newlabel{sec:toplevel-transition}{{8.1.1}{48}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.8.1.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Toplevel transitions }{48}{subsection.8.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Toplevel control}{50}{subsection.8.1.2}}
+\newlabel{sec:ML-toplevel}{{8.2}{50}{ML toplevel \label {sec:ML-toplevel}\relax }{section.8.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.2}ML toplevel }{50}{section.8.2}}
+\newlabel{sec:theory-database}{{8.3}{52}{Theory database \label {sec:theory-database}\relax }{section.8.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.3}Theory database }{52}{section.8.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{55}{appendix.A}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{49}{section.A.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{50}{section.A.2}}
-\@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{51}{section*.29}}
-\@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{51}{section*.30}}
-\@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{52}{section*.31}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{54}{appendix.B}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{55}{section.A.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{56}{section.A.2}}
+\@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{57}{section*.32}}
+\@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{57}{section*.33}}
+\@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{58}{section*.34}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{60}{appendix.B}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:ML-linear-trans}{{B.1}{54}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{54}{section.B.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{57}{section.B.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{57}{section.B.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{57}{subsection.B.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{58}{subsection.B.3.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{59}{subsection.B.3.3}}
-\bibstyle{plain}
+\newlabel{sec:ML-linear-trans}{{B.1}{60}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{60}{section.B.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{63}{section.B.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{63}{section.B.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{63}{subsection.B.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{64}{subsection.B.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{65}{subsection.B.3.3}}
+\bibstyle{abbrv}
 \bibdata{../manual}
 \bibcite{Barendregt-Geuvers:2001}{1}
 \bibcite{Berghofer-Nipkow:2000:TPHOL}{2}
 \bibcite{debruijn72}{3}
-\bibcite{nipkow-prehofer}{4}
-\bibcite{paulson700}{5}
-\bibcite{paulson-ml2}{6}
-\bibcite{isabelle-isar-ref}{7}
-\@writefile{toc}{\contentsline {chapter}{Bibliography}{60}{section*.39}}
-\@writefile{toc}{\contentsline {chapter}{Index}{61}{section*.41}}
+\bibcite{Gentzen:1935}{4}
+\bibcite{Haftmann-Wenzel:2009}{5}
+\bibcite{Miller:1991}{6}
+\bibcite{nipkow-prehofer}{7}
+\bibcite{paulson700}{8}
+\bibcite{paulson-ml2}{9}
+\bibcite{extensions91}{10}
+\bibcite{isabelle-isar-ref}{11}
+\@writefile{toc}{\contentsline {chapter}{Bibliography}{66}{section*.42}}
+\@writefile{toc}{\contentsline {chapter}{Index}{67}{section*.44}}

--- a/ProgTutorial/document/isar-ref.aux	Sun Aug 02 08:44:41 2009 +0200
+++ b/ProgTutorial/document/isar-ref.aux	Mon Aug 03 13:53:04 2009 +0200
@@ -13,320 +13,407 @@
 \fi
 
 \providecommand*\HyPL@Entry[1]{}
-\HyPL@Entry{0 << /S /D >> }
-\HyPL@Entry{1 << /S /r >> }
-\citation{isabelle-intro}
-\citation{isabelle-ref}
+\HyPL@Entry{0<</S/D>>}
+\select@language{english}
+\@writefile{toc}{\select@language{english}}
+\@writefile{lof}{\select@language{english}}
+\@writefile{lot}{\select@language{english}}
+\HyPL@Entry{1<</S/r>>}
+\HyPL@Entry{7<</S/D>>}
+\@writefile{toc}{\contentsline {part}{I\hspace  {1em}Basic Concepts}{1}{part.1}}
 \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{toc}{\contentsline {chapter}{\numberline {1}Introduction}{2}{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}}
+\@writefile{toc}{\contentsline {section}{\numberline {1.1}Overview}{2}{section.1.1}}
 \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}}
+\citation{Nipkow-TYPES02}
+\citation{Wenzel-Paulson:2006}
+\citation{Wenzel:2006:Festschrift}
+\citation{Trybulec:1993:MizarFeatures}
+\citation{Rudnicki:1992:MizarOverview}
+\citation{Wiedijk:1999:Mizar}
+\citation{Wenzel-Wiedijk:2002}
+\citation{paulson-found}
+\citation{paulson700}
+\citation{Gentzen:1935}
+\citation{isa-tutorial}
+\citation{isabelle-ZF}
+\@writefile{toc}{\contentsline {chapter}{\numberline {2}The Isabelle/Isar Framework }{4}{chapter.2}}
 \@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}}
+\newlabel{ch:isar-framework}{{2}{4}{The Isabelle/Isar Framework \label {ch:isar-framework}\relax }{chapter.2}{}}
+\citation{paulson-found}
+\citation{paulson700}
+\citation{church40}
+\newlabel{sec:framework-pure}{{2.1}{6}{The Pure framework \label {sec:framework-pure}\relax }{section.2.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.1}The Pure framework }{6}{section.2.1}}
+\citation{Berghofer-Nipkow:2000:TPHOL}
+\citation{Schroeder-Heister:1984}
+\citation{paulson-natural}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.1}Primitive inferences}{7}{subsection.2.1.1}}
+\citation{Miller:1991}
+\newlabel{sec:framework-resolution}{{2.1.2}{8}{Reasoning with rules \label {sec:framework-resolution}\relax }{subsection.2.1.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.2}Reasoning with rules }{8}{subsection.2.1.2}}
+\newlabel{sec:framework-isar}{{2.2}{10}{The Isar proof language \label {sec:framework-isar}\relax }{section.2.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.2}The Isar proof language }{10}{section.2.2}}
+\newlabel{sec:framework-context}{{2.2.1}{11}{Context elements \label {sec:framework-context}\relax }{subsection.2.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}Context elements }{11}{subsection.2.2.1}}
+\citation{Wenzel-PhD}
+\newlabel{sec:framework-stmt}{{2.2.2}{13}{Structured statements \label {sec:framework-stmt}\relax }{subsection.2.2.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}Structured statements }{13}{subsection.2.2.2}}
+\newlabel{sec:framework-subproof}{{2.2.3}{14}{Structured proof refinement \label {sec:framework-subproof}\relax }{subsection.2.2.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.3}Structured proof refinement }{14}{subsection.2.2.3}}
+\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Isar/VM modes}}{15}{figure.2.1}}
+\newlabel{fig:isar-vm}{{2.1}{15}{Isar/VM modes\relax }{figure.2.1}{}}
+\citation{Wenzel-PhD}
+\citation{Bauer-Wenzel:2001}
+\newlabel{sec:framework-calc}{{2.2.4}{16}{Calculational reasoning \label {sec:framework-calc}\relax }{subsection.2.2.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.4}Calculational reasoning }{16}{subsection.2.2.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.3}Example: First-Order Logic}{17}{section.2.3}}
+\newlabel{sec:framework-ex-equal}{{2.3.1}{17}{Equational reasoning \label {sec:framework-ex-equal}\relax }{subsection.2.3.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Equational reasoning }{17}{subsection.2.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Basic group theory}{18}{subsection.2.3.2}}
+\citation{Gentzen:1935}
+\newlabel{sec:framework-ex-prop}{{2.3.3}{20}{Propositional logic \label {sec:framework-ex-prop}\relax }{subsection.2.3.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.3}Propositional logic }{20}{subsection.2.3.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.4}Classical logic}{22}{subsection.2.3.4}}
+\citation{church40}
+\newlabel{sec:framework-ex-quant}{{2.3.5}{23}{Quantifiers \label {sec:framework-ex-quant}\relax }{subsection.2.3.5}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.5}Quantifiers }{23}{subsection.2.3.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.6}Canonical reasoning patterns}{23}{subsection.2.3.6}}
+\@writefile{toc}{\contentsline {part}{II\hspace  {1em}General Language Elements}{26}{part.2}}
 \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}}
+\citation{proofgeneral}
+\@writefile{toc}{\contentsline {chapter}{\numberline {3}Outer syntax}{27}{chapter.3}}
 \@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}}
+\newlabel{sec:outer-lex}{{3.1}{28}{Lexical matters \label {sec:outer-lex}\relax }{section.3.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.1}Lexical matters }{28}{section.3.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.2}Common syntax entities}{30}{section.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Names}{30}{subsection.3.2.1}}
+\newlabel{sec:comments}{{3.2.2}{31}{Comments \label {sec:comments}\relax }{subsection.3.2.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Comments }{31}{subsection.3.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.3}Type classes, sorts and arities}{31}{subsection.3.2.3}}
+\newlabel{sec:types-terms}{{3.2.4}{32}{Types and terms \label {sec:types-terms}\relax }{subsection.3.2.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.4}Types and terms }{32}{subsection.3.2.4}}
+\newlabel{sec:term-decls}{{3.2.5}{33}{Term patterns and declarations \label {sec:term-decls}\relax }{subsection.3.2.5}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.5}Term patterns and declarations }{33}{subsection.3.2.5}}
+\newlabel{sec:syn-att}{{3.2.6}{34}{Attributes and theorems \label {sec:syn-att}\relax }{subsection.3.2.6}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.6}Attributes and theorems }{34}{subsection.3.2.6}}
 \citation{isabelle-sys}
 \citation{isabelle-sys}
 \citation{isabelle-hol-book}
-\@writefile{toc}{\contentsline {chapter}{\numberline {5}Document preparation }{74}{chapter.5}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {4}Document preparation }{37}{chapter.4}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:document-prep}{{4}{37}{Document preparation \label {ch:document-prep}\relax }{chapter.4}{}}
+\newlabel{sec:markup}{{4.1}{38}{Markup commands \label {sec:markup}\relax }{section.4.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.1}Markup commands }{38}{section.4.1}}
+\newlabel{sec:antiq}{{4.2}{40}{Document Antiquotations \label {sec:antiq}\relax }{section.4.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.2}Document Antiquotations }{40}{section.4.2}}
+\@writefile{toc}{\contentsline {subsubsection}{Styled antiquotations}{43}{section*.2}}
+\@writefile{toc}{\contentsline {subsubsection}{General options}{43}{section*.3}}
+\citation{isabelle-sys}
+\newlabel{sec:tags}{{4.3}{45}{Markup via command tags \label {sec:tags}\relax }{section.4.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}Markup via command tags }{45}{section.4.3}}
+\citation{isabelle-sys}
+\@writefile{toc}{\contentsline {section}{\numberline {4.4}Draft presentation}{46}{section.4.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {5}Theory specifications}{47}{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}{}}
+\newlabel{sec:begin-thy}{{5.1}{47}{Defining theories \label {sec:begin-thy}\relax }{section.5.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.1}Defining theories }{47}{section.5.1}}
+\newlabel{sec:target}{{5.2}{48}{Local theory targets \label {sec:target}\relax }{section.5.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.2}Local theory targets }{48}{section.5.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.3}Basic specification elements}{49}{section.5.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.4}Generic declarations}{51}{section.5.4}}
+\newlabel{sec:locale}{{5.5}{52}{Locales \label {sec:locale}\relax }{section.5.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.5}Locales }{52}{section.5.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.1}Locale specifications}{52}{subsection.5.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.2}Interpretation of locales}{56}{subsection.5.5.2}}
+\citation{Wenzel:1997:TPHOL}
+\citation{isabelle-classes}
+\newlabel{sec:class}{{5.6}{59}{Classes \label {sec:class}\relax }{section.5.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.6}Classes }{59}{section.5.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.1}The class target}{62}{subsection.5.6.1}}
+\newlabel{sec:axclass}{{5.6.2}{62}{Old-style axiomatic type classes \label {sec:axclass}\relax }{subsection.5.6.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.6.2}Old-style axiomatic type classes }{62}{subsection.5.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.7}Unrestricted overloading}{63}{section.5.7}}
+\newlabel{sec:ML}{{5.8}{64}{Incorporating ML code \label {sec:ML}\relax }{section.5.8}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.8}Incorporating ML code }{64}{section.5.8}}
 \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{toc}{\contentsline {section}{\numberline {5.9}Primitive specification elements}{66}{section.5.9}}
+\newlabel{sec:classes}{{5.9.1}{66}{Type classes and sorts \label {sec:classes}\relax }{subsection.5.9.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.1}Type classes and sorts }{66}{subsection.5.9.1}}
+\newlabel{sec:types-pure}{{5.9.2}{67}{Types and type abbreviations \label {sec:types-pure}\relax }{subsection.5.9.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.2}Types and type abbreviations }{67}{subsection.5.9.2}}
+\citation{nipkow-prehofer}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.3}Co-regularity of type classes and arities}{68}{subsection.5.9.3}}
+\newlabel{sec:consts}{{5.9.4}{68}{Constants and definitions \label {sec:consts}\relax }{subsection.5.9.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.9.4}Constants and definitions }{68}{subsection.5.9.4}}
+\newlabel{sec:axms-thms}{{5.10}{71}{Axioms and theorems \label {sec:axms-thms}\relax }{section.5.10}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.10}Axioms and theorems }{71}{section.5.10}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.11}Oracles}{71}{section.5.11}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.12}Name spaces}{72}{section.5.12}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {6}Proofs }{74}{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}}
+\newlabel{ch:proofs}{{6}{74}{Proofs \label {ch:proofs}\relax }{chapter.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Proof structure}{74}{section.6.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.1.1}Blocks}{74}{subsection.6.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.1.2}Omitting proofs}{75}{subsection.6.1.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Statements}{76}{section.6.2}}
+\newlabel{sec:proof-context}{{6.2.1}{76}{Context elements \label {sec:proof-context}\relax }{subsection.6.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.2.1}Context elements }{76}{subsection.6.2.1}}
+\newlabel{sec:term-abbrev}{{6.2.2}{77}{Term abbreviations \label {sec:term-abbrev}\relax }{subsection.6.2.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.2.2}Term abbreviations }{77}{subsection.6.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.2.3}Facts and forward chaining}{79}{subsection.6.2.3}}
+\newlabel{sec:goals}{{6.2.4}{80}{Goals \label {sec:goals}\relax }{subsection.6.2.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.2.4}Goals }{80}{subsection.6.2.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}Refinement steps}{83}{section.6.3}}
+\newlabel{sec:proof-meth}{{6.3.1}{83}{Proof method expressions \label {sec:proof-meth}\relax }{subsection.6.3.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.1}Proof method expressions }{83}{subsection.6.3.1}}
+\newlabel{sec:proof-steps}{{6.3.2}{85}{Initial and terminal proof steps \label {sec:proof-steps}\relax }{subsection.6.3.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.2}Initial and terminal proof steps }{85}{subsection.6.3.2}}
+\newlabel{sec:pure-meth-att}{{6.3.3}{87}{Fundamental methods and attributes \label {sec:pure-meth-att}\relax }{subsection.6.3.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.3}Fundamental methods and attributes }{87}{subsection.6.3.3}}
+\newlabel{sec:tactic-commands}{{6.3.4}{89}{Emulating tactic scripts \label {sec:tactic-commands}\relax }{subsection.6.3.4}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.4}Emulating tactic scripts }{89}{subsection.6.3.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.5}Defining proof methods}{91}{subsection.6.3.5}}
+\newlabel{sec:obtain}{{6.4}{92}{Generalized elimination \label {sec:obtain}\relax }{section.6.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.4}Generalized elimination }{92}{section.6.4}}
+\newlabel{sec:calculation}{{6.5}{93}{Calculational reasoning \label {sec:calculation}\relax }{section.6.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.5}Calculational reasoning }{93}{section.6.5}}
+\newlabel{sec:cases-induct}{{6.6}{95}{Proof by cases and induction \label {sec:cases-induct}\relax }{section.6.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.6}Proof by cases and induction }{95}{section.6.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.6.1}Rule contexts}{95}{subsection.6.6.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.6.2}Proof methods}{98}{subsection.6.6.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.6.3}Declaring rules}{102}{subsection.6.6.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {7}Inner syntax --- the term language }{104}{chapter.7}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:inner-syntax}{{7}{104}{Inner syntax --- the term language \label {ch:inner-syntax}\relax }{chapter.7}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.1}Printing logical entities}{104}{section.7.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Diagnostic commands}{104}{subsection.7.1.1}}
 \citation{isabelle-ref}
 \citation{isabelle-sys}
-\@writefile{toc}{\contentsline {section}{\numberline {6.2}Inspecting the context}{86}{section.6.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Details of printed content}{106}{subsection.7.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.3}Printing limits}{108}{subsection.7.1.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.2}Mixfix annotations}{108}{section.7.2}}
+\citation{paulson-ml2}
+\@writefile{toc}{\contentsline {section}{\numberline {7.3}Explicit term notation}{111}{section.7.3}}
+\newlabel{sec:pure-syntax}{{7.4}{111}{The Pure syntax \label {sec:pure-syntax}\relax }{section.7.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.4}The Pure syntax }{111}{section.7.4}}
+\newlabel{sec:priority-grammar}{{7.4.1}{111}{Priority grammars \label {sec:priority-grammar}\relax }{subsection.7.4.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.1}Priority grammars }{111}{subsection.7.4.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.2}The Pure grammar}{113}{subsection.7.4.2}}
+\newlabel{sec:inner-lex}{{7.5}{116}{Lexical matters \label {sec:inner-lex}\relax }{section.7.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.5}Lexical matters }{116}{section.7.5}}
+\newlabel{sec:syn-trans}{{7.6}{117}{Syntax and translations \label {sec:syn-trans}\relax }{section.7.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.6}Syntax and translations }{117}{section.7.6}}
 \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}}
+\newlabel{sec:tr-funs}{{7.7}{119}{Syntax translation functions \label {sec:tr-funs}\relax }{section.7.7}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.7}Syntax translation functions }{119}{section.7.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.8}Inspecting the syntax}{120}{section.7.8}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {8}Other commands}{122}{chapter.8}}
 \@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}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.1}Inspecting the context}{122}{section.8.1}}
+\citation{isabelle-sys}
+\newlabel{sec:history}{{8.2}{124}{History commands \label {sec:history}\relax }{section.8.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.2}History commands }{124}{section.8.2}}
+\citation{proofgeneral}
+\citation{Aspinall:TACAS:2000}
+\@writefile{toc}{\contentsline {section}{\numberline {8.3}System commands}{125}{section.8.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {9}Generic tools and packages }{126}{chapter.9}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{ch:gen-tools}{{9}{126}{Generic tools and packages \label {ch:gen-tools}\relax }{chapter.9}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.1}Configuration options}{126}{section.9.1}}
+\citation{isabelle-implementation}
+\@writefile{toc}{\contentsline {section}{\numberline {9.2}Basic proof tools}{127}{section.9.2}}
+\newlabel{sec:misc-meth-att}{{9.2.1}{127}{Miscellaneous methods and attributes \label {sec:misc-meth-att}\relax }{subsection.9.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Miscellaneous methods and attributes }{127}{subsection.9.2.1}}
+\citation{isabelle-implementation}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.2}Low-level equational reasoning}{129}{subsection.9.2.2}}
+\newlabel{sec:tactics}{{9.2.3}{130}{Further tactic emulations \label {sec:tactics}\relax }{subsection.9.2.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.3}Further tactic emulations }{130}{subsection.9.2.3}}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\citation{isabelle-implementation}
+\newlabel{sec:simplifier}{{9.3}{133}{The Simplifier \label {sec:simplifier}\relax }{section.9.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.3}The Simplifier }{133}{section.9.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.1}Simplification methods}{133}{subsection.9.3.1}}
 \citation{isabelle-ref}
 \citation{isabelle-ref}
 \citation{isabelle-ref}
 \citation{isabelle-ref}
-\citation{isabelle-ref}
-\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.2}Declaring rules}{135}{subsection.9.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.3}Simplification procedures}{136}{subsection.9.3.3}}
 \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}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.4}Forward simplification}{137}{subsection.9.3.4}}
+\newlabel{sec:classical}{{9.4}{137}{The Classical Reasoner \label {sec:classical}\relax }{section.9.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.4}The Classical Reasoner }{137}{section.9.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.4.1}Basic methods}{137}{subsection.9.4.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.4.2}Automated methods}{138}{subsection.9.4.2}}
 \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}}
+\newlabel{sec:clasimp}{{9.4.3}{139}{Combined automated methods \label {sec:clasimp}\relax }{subsection.9.4.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.4.3}Combined automated methods }{139}{subsection.9.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{toc}{\contentsline {subsection}{\numberline {9.4.4}Declaring rules}{141}{subsection.9.4.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.4.5}Classical operations}{142}{subsection.9.4.5}}
+\newlabel{sec:object-logic}{{9.5}{142}{Object-logic setup \label {sec:object-logic}\relax }{section.9.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.5}Object-logic setup }{142}{section.9.5}}
+\@writefile{toc}{\contentsline {part}{III\hspace  {1em}Object-Logics}{144}{part.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {10}Isabelle/HOL }{145}{chapter.10}}
 \@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}}
+\newlabel{ch:hol}{{10}{145}{Isabelle/HOL \label {ch:hol}\relax }{chapter.10}{}}
+\newlabel{sec:hol-typedef}{{10.1}{145}{Primitive types \label {sec:hol-typedef}\relax }{section.10.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.1}Primitive types }{145}{section.10.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.2}Adhoc tuples}{146}{section.10.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}}
+\newlabel{sec:hol-record}{{10.3}{147}{Records \label {sec:hol-record}\relax }{section.10.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.3}Records }{147}{section.10.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Basic concepts}{147}{subsection.10.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}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.2}Record specifications}{148}{subsection.10.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.3}Record operations}{149}{subsection.10.3.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.4}Derived rules and proof tools}{150}{subsection.10.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}}
+\newlabel{sec:hol-datatype}{{10.4}{151}{Datatypes \label {sec:hol-datatype}\relax }{section.10.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.4}Datatypes }{151}{section.10.4}}
+\newlabel{sec:recursion}{{10.5}{152}{Recursive functions \label {sec:recursion}\relax }{section.10.5}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.5}Recursive functions }{152}{section.10.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}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.5.1}Proof methods related to recursive definitions}{154}{subsection.10.5.1}}
 \citation{isabelle-HOL}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.5.2}Old-style recursive function definitions (TFL)}{118}{subsection.8.5.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.5.2}Old-style recursive function definitions (TFL)}{155}{subsection.10.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}}
+\newlabel{sec:hol-inductive}{{10.6}{156}{Inductive and coinductive definitions \label {sec:hol-inductive}\relax }{section.10.6}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.6}Inductive and coinductive definitions }{156}{section.10.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.6.1}Derived rules}{158}{subsection.10.6.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.6.2}Monotonicity theorems}{158}{subsection.10.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.7}Arithmetic proof support}{159}{section.10.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.8}Intuitionistic proof search}{159}{section.10.8}}
+\citation{Bezem-Coquand:2005}
+\@writefile{toc}{\contentsline {section}{\numberline {10.9}Coherent Logic}{160}{section.10.9}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.10}Checking and refuting propositions}{160}{section.10.10}}
+\citation{isabelle-ref}
+\@writefile{toc}{\contentsline {section}{\numberline {10.11}Invoking automated reasoning tools -- The Sledgehammer}{162}{section.10.11}}
+\newlabel{sec:hol-induct-tac}{{10.12}{163}{Unstructured case analysis and induction \label {sec:hol-induct-tac}\relax }{section.10.12}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.12}Unstructured case analysis and induction }{163}{section.10.12}}
 \citation{isabelle-HOL}
-\@writefile{toc}{\contentsline {section}{\numberline {8.10}Executable code}{125}{section.8.10}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.13}Executable code}{165}{section.10.13}}
 \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}}
+\newlabel{sec:hol-specification}{{10.14}{174}{Definition by specification \label {sec:hol-specification}\relax }{section.10.14}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.14}Definition by specification }{174}{section.10.14}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {11}Isabelle/HOLCF }{176}{chapter.11}}
 \@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}}
+\newlabel{ch:holcf}{{11}{176}{Isabelle/HOLCF \label {ch:holcf}\relax }{chapter.11}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {11.1}Mixfix syntax for continuous operations}{176}{section.11.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {11.2}Recursive domains}{176}{section.11.2}}
 \citation{MuellerNvOS99}
-\@writefile{toc}{\contentsline {chapter}{\numberline {10}Isabelle/ZF }{137}{chapter.10}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {12}Isabelle/ZF }{178}{chapter.12}}
 \@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}}
+\newlabel{ch:zf}{{12}{178}{Isabelle/ZF \label {ch:zf}\relax }{chapter.12}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {12.1}Type checking}{178}{section.12.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {12.2}(Co)Inductive sets and datatypes}{178}{section.12.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {12.2.1}Set definitions}{178}{subsection.12.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{toc}{\contentsline {subsection}{\numberline {12.2.2}Primitive recursive functions}{180}{subsection.12.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {12.2.3}Cases and induction: emulating tactic scripts}{181}{subsection.12.2.3}}
+\@writefile{toc}{\contentsline {part}{IV\hspace  {1em}Appendix}{182}{part.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {A}Isabelle/Isar quick reference }{183}{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}}
+\newlabel{ap:refcard}{{A}{183}{Isabelle/Isar quick reference \label {ap:refcard}\relax }{appendix.A}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.1}Proof commands}{183}{section.A.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.1}Primitives and basic syntax}{183}{subsection.A.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.2}Abbreviations and synonyms}{184}{subsection.A.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.3}Derived elements}{184}{subsection.A.1.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.1.4}Diagnostic commands}{184}{subsection.A.1.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.2}Proof methods}{185}{section.A.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.3}Attributes}{186}{section.A.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.4}Rule declarations and methods}{186}{section.A.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.5}Emulating tactic scripts}{187}{section.A.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.5.1}Commands}{187}{subsection.A.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {A.5.2}Methods}{187}{subsection.A.5.2}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {B}Predefined Isabelle symbols }{188}{appendix.B}}
+\@writefile{lof}{\addvspace {10\p@ }}
+\@writefile{lot}{\addvspace {10\p@ }}
+\newlabel{app:symbols}{{B}{188}{Predefined Isabelle symbols \label {app:symbols}\relax }{appendix.B}{}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {C}ML tactic expressions}{194}{appendix.C}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {B.1}Resolution tactics}{146}{section.B.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {C.1}Resolution tactics}{194}{section.C.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}}
+\@writefile{toc}{\contentsline {section}{\numberline {C.2}Simplifier tactics}{195}{section.C.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {C.3}Classical Reasoner tactics}{195}{section.C.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {C.4}Miscellaneous tactics}{195}{section.C.4}}
 \citation{isabelle-ref}
 \citation{isabelle-ref}
-\bibstyle{plain}
+\bibstyle{abbrv}
 \bibdata{../manual}
-\@writefile{toc}{\contentsline {section}{\numberline {B.5}Tacticals}{148}{section.B.5}}
+\@writefile{toc}{\contentsline {section}{\numberline {C.5}Tacticals}{196}{section.C.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}
+\bibcite{Bauer-Wenzel:2001}{3}
+\bibcite{Berghofer-Nipkow:2000:TPHOL}{4}
+\bibcite{Bezem-Coquand:2005}{5}
+\bibcite{church40}{6}
+\bibcite{Gentzen:1935}{7}
+\bibcite{isabelle-codegen}{8}
+\bibcite{isabelle-classes}{9}
+\bibcite{isabelle-function}{10}
+\bibcite{OCaml}{11}
+\bibcite{Miller:1991}{12}
+\bibcite{SML}{13}
+\bibcite{MuellerNvOS99}{14}
+\bibcite{NaraschewskiW-TPHOLs98}{15}
+\bibcite{Nipkow-TYPES02}{16}
+\bibcite{isabelle-HOL}{17}
+\bibcite{isabelle-hol-book}{18}
+\bibcite{isa-tutorial}{19}
+\bibcite{nipkow-prehofer}{20}
+\bibcite{isabelle-ref}{21}
+\bibcite{isabelle-ZF}{22}
+\bibcite{paulson-natural}{23}
+\bibcite{paulson-found}{24}
+\bibcite{paulson700}{25}
+\bibcite{paulson-CADE}{26}
+\bibcite{paulson-ml2}{27}
+\bibcite{haskell-revised-report}{28}
+\bibcite{Rudnicki:1992:MizarOverview}{29}
+\bibcite{Schroeder-Heister:1984}{30}
+\bibcite{Trybulec:1993:MizarFeatures}{31}
+\bibcite{isabelle-implementation}{32}
+\bibcite{Wenzel:1997:TPHOL}{33}
+\bibcite{Wenzel:1999:TPHOL}{34}
+\bibcite{Wenzel-PhD}{35}
+\bibcite{Wenzel:2006:Festschrift}{36}
+\bibcite{isabelle-sys}{37}
+\bibcite{Wenzel-Paulson:2006}{38}
+\bibcite{Wiedijk:1999:Mizar}{39}
+\bibcite{Wenzel-Wiedijk:2002}{40}

--- a/ProgTutorial/document/root.tex	Sun Aug 02 08:44:41 2009 +0200
+++ b/ProgTutorial/document/root.tex	Mon Aug 03 13:53:04 2009 +0200
@@ -6,7 +6,6 @@
 \usepackage{charter}
 \usepackage[pdftex]{graphicx}
 \usepackage{proof}
-\usepackage{rail}
 \usepackage{url}
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
 \usepackage{lineno}

author	Christian Urban <urbanc@in.tum.de>
	Mon, 03 Aug 2009 13:53:04 +0200
changeset 300	f286dfa9f173
parent 299	d0b81d6e1b28
child 301	2728e8daebc0

ProgTutorial/document/implementation.aux		file \| annotate \| diff \| comparison \| revisions
ProgTutorial/document/isar-ref.aux		file \| annotate \| diff \| comparison \| revisions
ProgTutorial/document/root.tex		file \| annotate \| diff \| comparison \| revisions