73 \@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Admissible substitution rules}}{21}{figure.2.4}} |
73 \@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Admissible substitution rules}}{21}{figure.2.4}} |
74 \newlabel{fig:subst-rules}{{2.4}{21}{Admissible substitution rules\relax }{figure.2.4}{}} |
74 \newlabel{fig:subst-rules}{{2.4}{21}{Admissible substitution rules\relax }{figure.2.4}{}} |
75 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Auxiliary definitions}{24}{subsection.2.3.2}} |
75 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Auxiliary definitions}{24}{subsection.2.3.2}} |
76 \@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Definitions of auxiliary connectives}}{24}{figure.2.5}} |
76 \@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Definitions of auxiliary connectives}}{24}{figure.2.5}} |
77 \newlabel{fig:pure-aux}{{2.5}{24}{Definitions of auxiliary connectives\relax }{figure.2.5}{}} |
77 \newlabel{fig:pure-aux}{{2.5}{24}{Definitions of auxiliary connectives\relax }{figure.2.5}{}} |
|
78 \citation{Gentzen:1935} |
|
79 \citation{extensions91} |
78 \newlabel{sec:obj-rules}{{2.4}{25}{Object-level rules \label {sec:obj-rules}\relax }{section.2.4}{}} |
80 \newlabel{sec:obj-rules}{{2.4}{25}{Object-level rules \label {sec:obj-rules}\relax }{section.2.4}{}} |
79 \@writefile{toc}{\contentsline {section}{\numberline {2.4}Object-level rules }{25}{section.2.4}} |
81 \@writefile{toc}{\contentsline {section}{\numberline {2.4}Object-level rules }{25}{section.2.4}} |
80 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{26}{chapter.3}} |
82 \@writefile{toc}{\contentsline {subsection}{\numberline {2.4.1}Hereditary Harrop Formulae}{25}{subsection.2.4.1}} |
|
83 \citation{Miller:1991} |
|
84 \@writefile{toc}{\contentsline {subsection}{\numberline {2.4.2}Rule composition}{27}{subsection.2.4.2}} |
|
85 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{29}{chapter.3}} |
81 \@writefile{lof}{\addvspace {10\p@ }} |
86 \@writefile{lof}{\addvspace {10\p@ }} |
82 \@writefile{lot}{\addvspace {10\p@ }} |
87 \@writefile{lot}{\addvspace {10\p@ }} |
83 \newlabel{sec:tactical-goals}{{3.1}{26}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}} |
88 \newlabel{sec:tactical-goals}{{3.1}{29}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}} |
84 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{26}{section.3.1}} |
89 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{29}{section.3.1}} |
85 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{27}{section.3.2}} |
90 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{30}{section.3.2}} |
86 \newlabel{sec:resolve-assume-tac}{{3.2.1}{29}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}} |
91 \newlabel{sec:resolve-assume-tac}{{3.2.1}{32}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}} |
87 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{29}{subsection.3.2.1}} |
92 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{32}{subsection.3.2.1}} |
88 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{31}{subsection.3.2.2}} |
93 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{34}{subsection.3.2.2}} |
89 \newlabel{sec:tacticals}{{3.3}{32}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}} |
94 \newlabel{sec:tacticals}{{3.3}{35}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}} |
90 \@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{32}{section.3.3}} |
95 \@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{35}{section.3.3}} |
91 \@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{33}{chapter.4}} |
96 \@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{36}{chapter.4}} |
92 \@writefile{lof}{\addvspace {10\p@ }} |
97 \@writefile{lof}{\addvspace {10\p@ }} |
93 \@writefile{lot}{\addvspace {10\p@ }} |
98 \@writefile{lot}{\addvspace {10\p@ }} |
94 \newlabel{sec:variables}{{4.1}{33}{Variables \label {sec:variables}\relax }{section.4.1}{}} |
99 \newlabel{sec:variables}{{4.1}{36}{Variables \label {sec:variables}\relax }{section.4.1}{}} |
95 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{33}{section.4.1}} |
100 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{36}{section.4.1}} |
96 \newlabel{sec:assumptions}{{4.2}{35}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}} |
101 \newlabel{sec:assumptions}{{4.2}{38}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}} |
97 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{35}{section.4.2}} |
102 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{38}{section.4.2}} |
98 \citation{isabelle-isar-ref} |
103 \citation{isabelle-isar-ref} |
99 \newlabel{sec:results}{{4.3}{37}{Results \label {sec:results}\relax }{section.4.3}{}} |
104 \newlabel{sec:results}{{4.3}{40}{Results \label {sec:results}\relax }{section.4.3}{}} |
100 \@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{37}{section.4.3}} |
105 \@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{40}{section.4.3}} |
101 \@writefile{toc}{\contentsline {chapter}{\numberline {5}Isar proof texts}{39}{chapter.5}} |
106 \@writefile{toc}{\contentsline {chapter}{\numberline {5}Syntax and type-checking}{42}{chapter.5}} |
102 \@writefile{lof}{\addvspace {10\p@ }} |
107 \@writefile{lof}{\addvspace {10\p@ }} |
103 \@writefile{lot}{\addvspace {10\p@ }} |
108 \@writefile{lot}{\addvspace {10\p@ }} |
104 \@writefile{toc}{\contentsline {section}{\numberline {5.1}Proof context}{39}{section.5.1}} |
109 \@writefile{toc}{\contentsline {chapter}{\numberline {6}Isar language elements}{43}{chapter.6}} |
105 \newlabel{sec:isar-proof-state}{{5.2}{39}{Proof state \label {sec:isar-proof-state}\relax }{section.5.2}{}} |
|
106 \@writefile{toc}{\contentsline {section}{\numberline {5.2}Proof state }{39}{section.5.2}} |
|
107 \@writefile{toc}{\contentsline {section}{\numberline {5.3}Proof methods}{39}{section.5.3}} |
|
108 \@writefile{toc}{\contentsline {section}{\numberline {5.4}Attributes}{39}{section.5.4}} |
|
109 \@writefile{toc}{\contentsline {chapter}{\numberline {6}Structured specifications}{40}{chapter.6}} |
|
110 \@writefile{lof}{\addvspace {10\p@ }} |
110 \@writefile{lof}{\addvspace {10\p@ }} |
111 \@writefile{lot}{\addvspace {10\p@ }} |
111 \@writefile{lot}{\addvspace {10\p@ }} |
112 \@writefile{toc}{\contentsline {section}{\numberline {6.1}Specification elements}{40}{section.6.1}} |
112 \@writefile{toc}{\contentsline {section}{\numberline {6.1}Proof commands}{43}{section.6.1}} |
113 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Type-inference}{40}{section.6.2}} |
113 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Proof methods}{43}{section.6.2}} |
114 \@writefile{toc}{\contentsline {section}{\numberline {6.3}Local theories}{40}{section.6.3}} |
114 \@writefile{toc}{\contentsline {section}{\numberline {6.3}Attributes}{43}{section.6.3}} |
115 \@writefile{toc}{\contentsline {chapter}{\numberline {7}System integration}{41}{chapter.7}} |
115 \@writefile{toc}{\contentsline {chapter}{\numberline {7}Local theory specifications}{44}{chapter.7}} |
116 \@writefile{lof}{\addvspace {10\p@ }} |
116 \@writefile{lof}{\addvspace {10\p@ }} |
117 \@writefile{lot}{\addvspace {10\p@ }} |
117 \@writefile{lot}{\addvspace {10\p@ }} |
118 \newlabel{sec:isar-toplevel}{{7.1}{41}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.7.1}{}} |
118 \@writefile{toc}{\contentsline {section}{\numberline {7.1}Definitional elements}{44}{section.7.1}} |
119 \@writefile{toc}{\contentsline {section}{\numberline {7.1}Isar toplevel }{41}{section.7.1}} |
119 \citation{Haftmann-Wenzel:2009} |
120 \newlabel{sec:toplevel-transition}{{7.1.1}{42}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.7.1.1}{}} |
120 \@writefile{toc}{\contentsline {section}{\numberline {7.2}Morphisms and declarations}{46}{section.7.2}} |
121 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Toplevel transitions }{42}{subsection.7.1.1}} |
121 \@writefile{toc}{\contentsline {chapter}{\numberline {8}System integration}{47}{chapter.8}} |
122 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Toplevel control}{44}{subsection.7.1.2}} |
|
123 \newlabel{sec:ML-toplevel}{{7.2}{44}{ML toplevel \label {sec:ML-toplevel}\relax }{section.7.2}{}} |
|
124 \@writefile{toc}{\contentsline {section}{\numberline {7.2}ML toplevel }{44}{section.7.2}} |
|
125 \newlabel{sec:theory-database}{{7.3}{46}{Theory database \label {sec:theory-database}\relax }{section.7.3}{}} |
|
126 \@writefile{toc}{\contentsline {section}{\numberline {7.3}Theory database }{46}{section.7.3}} |
|
127 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{49}{appendix.A}} |
|
128 \@writefile{lof}{\addvspace {10\p@ }} |
122 \@writefile{lof}{\addvspace {10\p@ }} |
129 \@writefile{lot}{\addvspace {10\p@ }} |
123 \@writefile{lot}{\addvspace {10\p@ }} |
130 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{49}{section.A.1}} |
124 \newlabel{sec:isar-toplevel}{{8.1}{47}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.8.1}{}} |
131 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{50}{section.A.2}} |
125 \@writefile{toc}{\contentsline {section}{\numberline {8.1}Isar toplevel }{47}{section.8.1}} |
132 \@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{51}{section*.29}} |
126 \newlabel{sec:toplevel-transition}{{8.1.1}{48}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.8.1.1}{}} |
133 \@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{51}{section*.30}} |
127 \@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Toplevel transitions }{48}{subsection.8.1.1}} |
134 \@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{52}{section*.31}} |
128 \@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Toplevel control}{50}{subsection.8.1.2}} |
135 \@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{54}{appendix.B}} |
129 \newlabel{sec:ML-toplevel}{{8.2}{50}{ML toplevel \label {sec:ML-toplevel}\relax }{section.8.2}{}} |
|
130 \@writefile{toc}{\contentsline {section}{\numberline {8.2}ML toplevel }{50}{section.8.2}} |
|
131 \newlabel{sec:theory-database}{{8.3}{52}{Theory database \label {sec:theory-database}\relax }{section.8.3}{}} |
|
132 \@writefile{toc}{\contentsline {section}{\numberline {8.3}Theory database }{52}{section.8.3}} |
|
133 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{55}{appendix.A}} |
136 \@writefile{lof}{\addvspace {10\p@ }} |
134 \@writefile{lof}{\addvspace {10\p@ }} |
137 \@writefile{lot}{\addvspace {10\p@ }} |
135 \@writefile{lot}{\addvspace {10\p@ }} |
138 \newlabel{sec:ML-linear-trans}{{B.1}{54}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}} |
136 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{55}{section.A.1}} |
139 \@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{54}{section.B.1}} |
137 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{56}{section.A.2}} |
140 \@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{57}{section.B.2}} |
138 \@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{57}{section*.32}} |
141 \@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{57}{section.B.3}} |
139 \@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{57}{section*.33}} |
142 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{57}{subsection.B.3.1}} |
140 \@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{58}{section*.34}} |
143 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{58}{subsection.B.3.2}} |
141 \@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{60}{appendix.B}} |
144 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{59}{subsection.B.3.3}} |
142 \@writefile{lof}{\addvspace {10\p@ }} |
145 \bibstyle{plain} |
143 \@writefile{lot}{\addvspace {10\p@ }} |
|
144 \newlabel{sec:ML-linear-trans}{{B.1}{60}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}} |
|
145 \@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{60}{section.B.1}} |
|
146 \@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{63}{section.B.2}} |
|
147 \@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{63}{section.B.3}} |
|
148 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{63}{subsection.B.3.1}} |
|
149 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{64}{subsection.B.3.2}} |
|
150 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{65}{subsection.B.3.3}} |
|
151 \bibstyle{abbrv} |
146 \bibdata{../manual} |
152 \bibdata{../manual} |
147 \bibcite{Barendregt-Geuvers:2001}{1} |
153 \bibcite{Barendregt-Geuvers:2001}{1} |
148 \bibcite{Berghofer-Nipkow:2000:TPHOL}{2} |
154 \bibcite{Berghofer-Nipkow:2000:TPHOL}{2} |
149 \bibcite{debruijn72}{3} |
155 \bibcite{debruijn72}{3} |
150 \bibcite{nipkow-prehofer}{4} |
156 \bibcite{Gentzen:1935}{4} |
151 \bibcite{paulson700}{5} |
157 \bibcite{Haftmann-Wenzel:2009}{5} |
152 \bibcite{paulson-ml2}{6} |
158 \bibcite{Miller:1991}{6} |
153 \bibcite{isabelle-isar-ref}{7} |
159 \bibcite{nipkow-prehofer}{7} |
154 \@writefile{toc}{\contentsline {chapter}{Bibliography}{60}{section*.39}} |
160 \bibcite{paulson700}{8} |
155 \@writefile{toc}{\contentsline {chapter}{Index}{61}{section*.41}} |
161 \bibcite{paulson-ml2}{9} |
|
162 \bibcite{extensions91}{10} |
|
163 \bibcite{isabelle-isar-ref}{11} |
|
164 \@writefile{toc}{\contentsline {chapter}{Bibliography}{66}{section*.42}} |
|
165 \@writefile{toc}{\contentsline {chapter}{Index}{67}{section*.44}} |