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