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