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

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

\@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}{2}{section.1.1}}

\citation{Wenzel:1999:TPHOL}

\citation{Wenzel-PhD}

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

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

\@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: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 {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}

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

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

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

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

\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 {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}{{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}{{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 {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}{{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 {10.5.1}Proof methods related to recursive definitions}{154}{subsection.10.5.1}}

\citation{isabelle-HOL}

\@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}{{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 {10.13}Executable code}{165}{section.10.13}}

\citation{SML}

\citation{OCaml}

\citation{haskell-revised-report}

\citation{isabelle-codegen}

\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}{{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 {12}Isabelle/ZF }{178}{chapter.12}}

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

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

\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 {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}{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 {C.1}Resolution tactics}{194}{section.C.1}}

\citation{isabelle-ref}

\citation{isabelle-ref}

\@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{abbrv}

\bibdata{../manual}

\@writefile{toc}{\contentsline {section}{\numberline {C.5}Tacticals}{196}{section.C.5}}

\bibcite{proofgeneral}{1}

\bibcite{Aspinall:TACAS:2000}{2}

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