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