--- 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}}