1 \relax 

     2 \catcode 95\active

     3 \ifx\hyper@anchor\@undefined

     4 \global \let \oldcontentsline\contentsline

     5 \gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}

     6 \global \let \oldnewlabel\newlabel

     7 \gdef \newlabel#1#2{\newlabelxx{#1}#2}

     8 \gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}

     9 \AtEndDocument{\let \contentsline\oldcontentsline

    10 \let \newlabel\oldnewlabel}

    11 \else

    12 \global \let \hyper@last\relax 

    13 \fi

    14 

    15 \providecommand*\HyPL@Entry[1]{}

    16 \HyPL@Entry{0<</S/D>>}

    17 \HyPL@Entry{1<</S/D>>}

    18 \HyPL@Entry{2<</S/D>>}

    19 \HyPL@Entry{3<</S/r>>}

    20 \citation{isabelle-isar-ref}

    21 \HyPL@Entry{7<</S/D>>}

    22 \@writefile{toc}{\contentsline {chapter}{\numberline {1}Preliminaries}{1}{chapter.1}}

    23 \@writefile{lof}{\addvspace {10\p@ }}

    24 \@writefile{lot}{\addvspace {10\p@ }}

    25 \newlabel{sec:context}{{1.1}{1}{Contexts \label {sec:context}\relax }{section.1.1}{}}

    26 \@writefile{toc}{\contentsline {section}{\numberline {1.1}Contexts }{1}{section.1.1}}

    27 \newlabel{sec:context-theory}{{1.1.1}{2}{Theory context \label {sec:context-theory}\relax }{subsection.1.1.1}{}}

    28 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.1}Theory context }{2}{subsection.1.1.1}}

    29 \@writefile{lof}{\contentsline {figure}{\numberline {1.1}{\ignorespaces A theory definition depending on ancestors}}{3}{figure.1.1}}

    30 \newlabel{fig:ex-theory}{{1.1}{3}{A theory definition depending on ancestors\relax }{figure.1.1}{}}

    31 \newlabel{sec:context-proof}{{1.1.2}{4}{Proof context \label {sec:context-proof}\relax }{subsection.1.1.2}{}}

    32 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.2}Proof context }{4}{subsection.1.1.2}}

    33 \newlabel{sec:generic-context}{{1.1.3}{5}{Generic contexts \label {sec:generic-context}\relax }{subsection.1.1.3}{}}

    34 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.3}Generic contexts }{5}{subsection.1.1.3}}

    35 \newlabel{sec:context-data}{{1.1.4}{6}{Context data \label {sec:context-data}\relax }{subsection.1.1.4}{}}

    36 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.4}Context data }{6}{subsection.1.1.4}}

    37 \@writefile{toc}{\contentsline {paragraph}{Theory data}{6}{section*.6}}

    38 \@writefile{toc}{\contentsline {paragraph}{Proof context data}{6}{section*.7}}

    39 \@writefile{toc}{\contentsline {paragraph}{Generic data}{6}{section*.8}}

    40 \newlabel{sec:names}{{1.2}{7}{Names \label {sec:names}\relax }{section.1.2}{}}

    41 \@writefile{toc}{\contentsline {section}{\numberline {1.2}Names }{7}{section.1.2}}

    42 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}Strings of symbols}{7}{subsection.1.2.1}}

    43 \citation{isabelle-isar-ref}

    44 \newlabel{sec:basic-names}{{1.2.2}{9}{Basic names \label {sec:basic-names}\relax }{subsection.1.2.2}{}}

    45 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}Basic names }{9}{subsection.1.2.2}}

    46 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.3}Indexed names}{10}{subsection.1.2.3}}

    47 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.4}Qualified names and name spaces}{11}{subsection.1.2.4}}

    48 \citation{paulson700}

    49 \citation{Barendregt-Geuvers:2001}

    50 \@writefile{toc}{\contentsline {chapter}{\numberline {2}Primitive logic }{14}{chapter.2}}

    51 \@writefile{lof}{\addvspace {10\p@ }}

    52 \@writefile{lot}{\addvspace {10\p@ }}

    53 \newlabel{ch:logic}{{2}{14}{Primitive logic \label {ch:logic}\relax }{chapter.2}{}}

    54 \newlabel{sec:types}{{2.1}{14}{Types \label {sec:types}\relax }{section.2.1}{}}

    55 \@writefile{toc}{\contentsline {section}{\numberline {2.1}Types }{14}{section.2.1}}

    56 \citation{nipkow-prehofer}

    57 \citation{debruijn72}

    58 \citation{paulson-ml2}

    59 \newlabel{sec:terms}{{2.2}{17}{Terms \label {sec:terms}\relax }{section.2.2}{}}

    60 \@writefile{toc}{\contentsline {section}{\numberline {2.2}Terms }{17}{section.2.2}}

    61 \citation{Berghofer-Nipkow:2000:TPHOL}

    62 \citation{Barendregt-Geuvers:2001}

    63 \newlabel{sec:thms}{{2.3}{20}{Theorems \label {sec:thms}\relax }{section.2.3}{}}

    64 \@writefile{toc}{\contentsline {section}{\numberline {2.3}Theorems }{20}{section.2.3}}

    65 \newlabel{sec:prim-rules}{{2.3.1}{20}{Primitive connectives and rules \label {sec:prim-rules}\relax }{subsection.2.3.1}{}}

    66 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Primitive connectives and rules }{20}{subsection.2.3.1}}

    67 \@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Primitive connectives of Pure}}{20}{figure.2.1}}

    68 \newlabel{fig:pure-connectives}{{2.1}{20}{Primitive connectives of Pure\relax }{figure.2.1}{}}

    69 \@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Primitive inferences of Pure}}{21}{figure.2.2}}

    70 \newlabel{fig:prim-rules}{{2.2}{21}{Primitive inferences of Pure\relax }{figure.2.2}{}}

    71 \@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces Conceptual axiomatization of Pure equality}}{21}{figure.2.3}}

    72 \newlabel{fig:pure-equality}{{2.3}{21}{Conceptual axiomatization of Pure equality\relax }{figure.2.3}{}}

    73 \@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Admissible substitution rules}}{21}{figure.2.4}}

    74 \newlabel{fig:subst-rules}{{2.4}{21}{Admissible substitution rules\relax }{figure.2.4}{}}

    75 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Auxiliary definitions}{24}{subsection.2.3.2}}

    76 \@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Definitions of auxiliary connectives}}{24}{figure.2.5}}

    77 \newlabel{fig:pure-aux}{{2.5}{24}{Definitions of auxiliary connectives\relax }{figure.2.5}{}}

    78 \newlabel{sec:obj-rules}{{2.4}{25}{Object-level rules \label {sec:obj-rules}\relax }{section.2.4}{}}

    79 \@writefile{toc}{\contentsline {section}{\numberline {2.4}Object-level rules }{25}{section.2.4}}

    80 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{26}{chapter.3}}

    81 \@writefile{lof}{\addvspace {10\p@ }}

    82 \@writefile{lot}{\addvspace {10\p@ }}

    83 \newlabel{sec:tactical-goals}{{3.1}{26}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}}

    84 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{26}{section.3.1}}

    85 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{27}{section.3.2}}

    86 \newlabel{sec:resolve-assume-tac}{{3.2.1}{29}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}}

    87 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{29}{subsection.3.2.1}}

    88 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{31}{subsection.3.2.2}}

    89 \newlabel{sec:tacticals}{{3.3}{32}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}}

    90 \@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{32}{section.3.3}}

    91 \@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{33}{chapter.4}}

    92 \@writefile{lof}{\addvspace {10\p@ }}

    93 \@writefile{lot}{\addvspace {10\p@ }}

    94 \newlabel{sec:variables}{{4.1}{33}{Variables \label {sec:variables}\relax }{section.4.1}{}}

    95 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{33}{section.4.1}}

    96 \newlabel{sec:assumptions}{{4.2}{35}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}}

    97 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{35}{section.4.2}}

    98 \citation{isabelle-isar-ref}

    99 \newlabel{sec:results}{{4.3}{37}{Results \label {sec:results}\relax }{section.4.3}{}}

   100 \@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{37}{section.4.3}}

   101 \@writefile{toc}{\contentsline {chapter}{\numberline {5}Isar proof texts}{39}{chapter.5}}

   102 \@writefile{lof}{\addvspace {10\p@ }}

   103 \@writefile{lot}{\addvspace {10\p@ }}

   104 \@writefile{toc}{\contentsline {section}{\numberline {5.1}Proof context}{39}{section.5.1}}

   105 \newlabel{sec:isar-proof-state}{{5.2}{39}{Proof state \label {sec:isar-proof-state}\relax }{section.5.2}{}}

   106 \@writefile{toc}{\contentsline {section}{\numberline {5.2}Proof state }{39}{section.5.2}}

   107 \@writefile{toc}{\contentsline {section}{\numberline {5.3}Proof methods}{39}{section.5.3}}

   108 \@writefile{toc}{\contentsline {section}{\numberline {5.4}Attributes}{39}{section.5.4}}

   109 \@writefile{toc}{\contentsline {chapter}{\numberline {6}Structured specifications}{40}{chapter.6}}

   110 \@writefile{lof}{\addvspace {10\p@ }}

   111 \@writefile{lot}{\addvspace {10\p@ }}

   112 \@writefile{toc}{\contentsline {section}{\numberline {6.1}Specification elements}{40}{section.6.1}}

   113 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Type-inference}{40}{section.6.2}}

   114 \@writefile{toc}{\contentsline {section}{\numberline {6.3}Local theories}{40}{section.6.3}}

   115 \@writefile{toc}{\contentsline {chapter}{\numberline {7}System integration}{41}{chapter.7}}

   116 \@writefile{lof}{\addvspace {10\p@ }}

   117 \@writefile{lot}{\addvspace {10\p@ }}

   118 \newlabel{sec:isar-toplevel}{{7.1}{41}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.7.1}{}}

   119 \@writefile{toc}{\contentsline {section}{\numberline {7.1}Isar toplevel }{41}{section.7.1}}

   120 \newlabel{sec:toplevel-transition}{{7.1.1}{42}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.7.1.1}{}}

   121 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Toplevel transitions }{42}{subsection.7.1.1}}

   122 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Toplevel control}{44}{subsection.7.1.2}}

   123 \newlabel{sec:ML-toplevel}{{7.2}{44}{ML toplevel \label {sec:ML-toplevel}\relax }{section.7.2}{}}

   124 \@writefile{toc}{\contentsline {section}{\numberline {7.2}ML toplevel }{44}{section.7.2}}

   125 \newlabel{sec:theory-database}{{7.3}{46}{Theory database \label {sec:theory-database}\relax }{section.7.3}{}}

   126 \@writefile{toc}{\contentsline {section}{\numberline {7.3}Theory database }{46}{section.7.3}}

   127 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{49}{appendix.A}}

   128 \@writefile{lof}{\addvspace {10\p@ }}

   129 \@writefile{lot}{\addvspace {10\p@ }}

   130 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{49}{section.A.1}}

   131 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{50}{section.A.2}}

   132 \@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{51}{section*.29}}

   133 \@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{51}{section*.30}}

   134 \@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{52}{section*.31}}

   135 \@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{54}{appendix.B}}

   136 \@writefile{lof}{\addvspace {10\p@ }}

   137 \@writefile{lot}{\addvspace {10\p@ }}

   138 \newlabel{sec:ML-linear-trans}{{B.1}{54}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}}

   139 \@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{54}{section.B.1}}

   140 \@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{57}{section.B.2}}

   141 \@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{57}{section.B.3}}

   142 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{57}{subsection.B.3.1}}

   143 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{58}{subsection.B.3.2}}

   144 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{59}{subsection.B.3.3}}

   145 \bibstyle{plain}

   146 \bibdata{../manual}

   147 \bibcite{Barendregt-Geuvers:2001}{1}

   148 \bibcite{Berghofer-Nipkow:2000:TPHOL}{2}

   149 \bibcite{debruijn72}{3}

   150 \bibcite{nipkow-prehofer}{4}

   151 \bibcite{paulson700}{5}

   152 \bibcite{paulson-ml2}{6}

   153 \bibcite{isabelle-isar-ref}{7}

   154 \@writefile{toc}{\contentsline {chapter}{Bibliography}{60}{section*.39}}

   155 \@writefile{toc}{\contentsline {chapter}{Index}{61}{section*.41}}