11 \else |
11 \else |
12 \global \let \hyper@last\relax |
12 \global \let \hyper@last\relax |
13 \fi |
13 \fi |
14 |
14 |
15 \providecommand*\HyPL@Entry[1]{} |
15 \providecommand*\HyPL@Entry[1]{} |
16 \HyPL@Entry{0 << /S /D >> } |
16 \HyPL@Entry{0<</S/D>>} |
17 \HyPL@Entry{1 << /S /r >> } |
17 \select@language{english} |
18 \citation{isabelle-intro} |
18 \@writefile{toc}{\select@language{english}} |
19 \citation{isabelle-ref} |
19 \@writefile{lof}{\select@language{english}} |
|
20 \@writefile{lot}{\select@language{english}} |
|
21 \HyPL@Entry{1<</S/r>>} |
|
22 \HyPL@Entry{7<</S/D>>} |
|
23 \@writefile{toc}{\contentsline {part}{I\hspace {1em}Basic Concepts}{1}{part.1}} |
20 \citation{proofgeneral} |
24 \citation{proofgeneral} |
21 \citation{Aspinall:TACAS:2000} |
25 \citation{Aspinall:TACAS:2000} |
22 \citation{Wenzel:1999:TPHOL} |
26 \citation{Wenzel:1999:TPHOL} |
23 \citation{Wenzel-PhD} |
27 \citation{Wenzel-PhD} |
24 \HyPL@Entry{5 << /S /D >> } |
28 \@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{2}{chapter.1}} |
25 \@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}} |
29 \@writefile{lof}{\addvspace {10\p@ }} |
26 \@writefile{lof}{\addvspace {10\p@ }} |
30 \@writefile{lot}{\addvspace {10\p@ }} |
27 \@writefile{lot}{\addvspace {10\p@ }} |
31 \@writefile{toc}{\contentsline {section}{\numberline {1.1}Overview}{2}{section.1.1}} |
28 \@writefile{toc}{\contentsline {section}{\numberline {1.1}Overview}{1}{section.1.1}} |
32 \citation{Wenzel:1999:TPHOL} |
|
33 \citation{Wenzel-PhD} |
|
34 \citation{Nipkow-TYPES02} |
|
35 \citation{Wenzel-Paulson:2006} |
29 \citation{Wenzel:2006:Festschrift} |
36 \citation{Wenzel:2006:Festschrift} |
|
37 \citation{Trybulec:1993:MizarFeatures} |
|
38 \citation{Rudnicki:1992:MizarOverview} |
|
39 \citation{Wiedijk:1999:Mizar} |
|
40 \citation{Wenzel-Wiedijk:2002} |
|
41 \citation{paulson-found} |
|
42 \citation{paulson700} |
|
43 \citation{Gentzen:1935} |
|
44 \citation{isa-tutorial} |
|
45 \citation{isabelle-ZF} |
|
46 \@writefile{toc}{\contentsline {chapter}{\numberline {2}The Isabelle/Isar Framework }{4}{chapter.2}} |
|
47 \@writefile{lof}{\addvspace {10\p@ }} |
|
48 \@writefile{lot}{\addvspace {10\p@ }} |
|
49 \newlabel{ch:isar-framework}{{2}{4}{The Isabelle/Isar Framework \label {ch:isar-framework}\relax }{chapter.2}{}} |
|
50 \citation{paulson-found} |
|
51 \citation{paulson700} |
|
52 \citation{church40} |
|
53 \newlabel{sec:framework-pure}{{2.1}{6}{The Pure framework \label {sec:framework-pure}\relax }{section.2.1}{}} |
|
54 \@writefile{toc}{\contentsline {section}{\numberline {2.1}The Pure framework }{6}{section.2.1}} |
|
55 \citation{Berghofer-Nipkow:2000:TPHOL} |
|
56 \citation{Schroeder-Heister:1984} |
|
57 \citation{paulson-natural} |
|
58 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1.1}Primitive inferences}{7}{subsection.2.1.1}} |
|
59 \citation{Miller:1991} |
|
60 \newlabel{sec:framework-resolution}{{2.1.2}{8}{Reasoning with rules \label {sec:framework-resolution}\relax }{subsection.2.1.2}{}} |
|
61 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1.2}Reasoning with rules }{8}{subsection.2.1.2}} |
|
62 \newlabel{sec:framework-isar}{{2.2}{10}{The Isar proof language \label {sec:framework-isar}\relax }{section.2.2}{}} |
|
63 \@writefile{toc}{\contentsline {section}{\numberline {2.2}The Isar proof language }{10}{section.2.2}} |
|
64 \newlabel{sec:framework-context}{{2.2.1}{11}{Context elements \label {sec:framework-context}\relax }{subsection.2.2.1}{}} |
|
65 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}Context elements }{11}{subsection.2.2.1}} |
|
66 \citation{Wenzel-PhD} |
|
67 \newlabel{sec:framework-stmt}{{2.2.2}{13}{Structured statements \label {sec:framework-stmt}\relax }{subsection.2.2.2}{}} |
|
68 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}Structured statements }{13}{subsection.2.2.2}} |
|
69 \newlabel{sec:framework-subproof}{{2.2.3}{14}{Structured proof refinement \label {sec:framework-subproof}\relax }{subsection.2.2.3}{}} |
|
70 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.3}Structured proof refinement }{14}{subsection.2.2.3}} |
|
71 \@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Isar/VM modes}}{15}{figure.2.1}} |
|
72 \newlabel{fig:isar-vm}{{2.1}{15}{Isar/VM modes\relax }{figure.2.1}{}} |
|
73 \citation{Wenzel-PhD} |
|
74 \citation{Bauer-Wenzel:2001} |
|
75 \newlabel{sec:framework-calc}{{2.2.4}{16}{Calculational reasoning \label {sec:framework-calc}\relax }{subsection.2.2.4}{}} |
|
76 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.4}Calculational reasoning }{16}{subsection.2.2.4}} |
|
77 \@writefile{toc}{\contentsline {section}{\numberline {2.3}Example: First-Order Logic}{17}{section.2.3}} |
|
78 \newlabel{sec:framework-ex-equal}{{2.3.1}{17}{Equational reasoning \label {sec:framework-ex-equal}\relax }{subsection.2.3.1}{}} |
|
79 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Equational reasoning }{17}{subsection.2.3.1}} |
|
80 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Basic group theory}{18}{subsection.2.3.2}} |
|
81 \citation{Gentzen:1935} |
|
82 \newlabel{sec:framework-ex-prop}{{2.3.3}{20}{Propositional logic \label {sec:framework-ex-prop}\relax }{subsection.2.3.3}{}} |
|
83 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.3}Propositional logic }{20}{subsection.2.3.3}} |
|
84 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.4}Classical logic}{22}{subsection.2.3.4}} |
|
85 \citation{church40} |
|
86 \newlabel{sec:framework-ex-quant}{{2.3.5}{23}{Quantifiers \label {sec:framework-ex-quant}\relax }{subsection.2.3.5}{}} |
|
87 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.5}Quantifiers }{23}{subsection.2.3.5}} |
|
88 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.6}Canonical reasoning patterns}{23}{subsection.2.3.6}} |
|
89 \@writefile{toc}{\contentsline {part}{II\hspace {1em}General Language Elements}{26}{part.2}} |
|
90 \citation{isabelle-sys} |
|
91 \citation{proofgeneral} |
|
92 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Outer syntax}{27}{chapter.3}} |
|
93 \@writefile{lof}{\addvspace {10\p@ }} |
|
94 \@writefile{lot}{\addvspace {10\p@ }} |
|
95 \newlabel{sec:outer-lex}{{3.1}{28}{Lexical matters \label {sec:outer-lex}\relax }{section.3.1}{}} |
|
96 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Lexical matters }{28}{section.3.1}} |
|
97 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Common syntax entities}{30}{section.3.2}} |
|
98 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Names}{30}{subsection.3.2.1}} |
|
99 \newlabel{sec:comments}{{3.2.2}{31}{Comments \label {sec:comments}\relax }{subsection.3.2.2}{}} |
|
100 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Comments }{31}{subsection.3.2.2}} |
|
101 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.3}Type classes, sorts and arities}{31}{subsection.3.2.3}} |
|
102 \newlabel{sec:types-terms}{{3.2.4}{32}{Types and terms \label {sec:types-terms}\relax }{subsection.3.2.4}{}} |
|
103 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.4}Types and terms }{32}{subsection.3.2.4}} |
|
104 \newlabel{sec:term-decls}{{3.2.5}{33}{Term patterns and declarations \label {sec:term-decls}\relax }{subsection.3.2.5}{}} |
|
105 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.5}Term patterns and declarations }{33}{subsection.3.2.5}} |
|
106 \newlabel{sec:syn-att}{{3.2.6}{34}{Attributes and theorems \label {sec:syn-att}\relax }{subsection.3.2.6}{}} |
|
107 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.6}Attributes and theorems }{34}{subsection.3.2.6}} |
|
108 \citation{isabelle-sys} |
|
109 \citation{isabelle-sys} |
|
110 \citation{isabelle-hol-book} |
|
111 \@writefile{toc}{\contentsline {chapter}{\numberline {4}Document preparation }{37}{chapter.4}} |
|
112 \@writefile{lof}{\addvspace {10\p@ }} |
|
113 \@writefile{lot}{\addvspace {10\p@ }} |
|
114 \newlabel{ch:document-prep}{{4}{37}{Document preparation \label {ch:document-prep}\relax }{chapter.4}{}} |
|
115 \newlabel{sec:markup}{{4.1}{38}{Markup commands \label {sec:markup}\relax }{section.4.1}{}} |
|
116 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Markup commands }{38}{section.4.1}} |
|
117 \newlabel{sec:antiq}{{4.2}{40}{Document Antiquotations \label {sec:antiq}\relax }{section.4.2}{}} |
|
118 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Document Antiquotations }{40}{section.4.2}} |
|
119 \@writefile{toc}{\contentsline {subsubsection}{Styled antiquotations}{43}{section*.2}} |
|
120 \@writefile{toc}{\contentsline {subsubsection}{General options}{43}{section*.3}} |
|
121 \citation{isabelle-sys} |
|
122 \newlabel{sec:tags}{{4.3}{45}{Markup via command tags \label {sec:tags}\relax }{section.4.3}{}} |
|
123 \@writefile{toc}{\contentsline {section}{\numberline {4.3}Markup via command tags }{45}{section.4.3}} |
|
124 \citation{isabelle-sys} |
|
125 \@writefile{toc}{\contentsline {section}{\numberline {4.4}Draft presentation}{46}{section.4.4}} |
|
126 \@writefile{toc}{\contentsline {chapter}{\numberline {5}Theory specifications}{47}{chapter.5}} |
|
127 \@writefile{lof}{\addvspace {10\p@ }} |
|
128 \@writefile{lot}{\addvspace {10\p@ }} |
|
129 \newlabel{sec:begin-thy}{{5.1}{47}{Defining theories \label {sec:begin-thy}\relax }{section.5.1}{}} |
|
130 \@writefile{toc}{\contentsline {section}{\numberline {5.1}Defining theories }{47}{section.5.1}} |
|
131 \newlabel{sec:target}{{5.2}{48}{Local theory targets \label {sec:target}\relax }{section.5.2}{}} |
|
132 \@writefile{toc}{\contentsline {section}{\numberline {5.2}Local theory targets }{48}{section.5.2}} |
|
133 \@writefile{toc}{\contentsline {section}{\numberline {5.3}Basic specification elements}{49}{section.5.3}} |
|
134 \@writefile{toc}{\contentsline {section}{\numberline {5.4}Generic declarations}{51}{section.5.4}} |
|
135 \newlabel{sec:locale}{{5.5}{52}{Locales \label {sec:locale}\relax }{section.5.5}{}} |
|
136 \@writefile{toc}{\contentsline {section}{\numberline {5.5}Locales }{52}{section.5.5}} |
|
137 \@writefile{toc}{\contentsline {subsection}{\numberline {5.5.1}Locale specifications}{52}{subsection.5.5.1}} |
|
138 \@writefile{toc}{\contentsline {subsection}{\numberline {5.5.2}Interpretation of locales}{56}{subsection.5.5.2}} |
|
139 \citation{Wenzel:1997:TPHOL} |
|
140 \citation{isabelle-classes} |
|
141 \newlabel{sec:class}{{5.6}{59}{Classes \label {sec:class}\relax }{section.5.6}{}} |
|
142 \@writefile{toc}{\contentsline {section}{\numberline {5.6}Classes }{59}{section.5.6}} |
|
143 \@writefile{toc}{\contentsline {subsection}{\numberline {5.6.1}The class target}{62}{subsection.5.6.1}} |
|
144 \newlabel{sec:axclass}{{5.6.2}{62}{Old-style axiomatic type classes \label {sec:axclass}\relax }{subsection.5.6.2}{}} |
|
145 \@writefile{toc}{\contentsline {subsection}{\numberline {5.6.2}Old-style axiomatic type classes }{62}{subsection.5.6.2}} |
|
146 \@writefile{toc}{\contentsline {section}{\numberline {5.7}Unrestricted overloading}{63}{section.5.7}} |
|
147 \newlabel{sec:ML}{{5.8}{64}{Incorporating ML code \label {sec:ML}\relax }{section.5.8}{}} |
|
148 \@writefile{toc}{\contentsline {section}{\numberline {5.8}Incorporating ML code }{64}{section.5.8}} |
|
149 \citation{isabelle-sys} |
|
150 \@writefile{toc}{\contentsline {section}{\numberline {5.9}Primitive specification elements}{66}{section.5.9}} |
|
151 \newlabel{sec:classes}{{5.9.1}{66}{Type classes and sorts \label {sec:classes}\relax }{subsection.5.9.1}{}} |
|
152 \@writefile{toc}{\contentsline {subsection}{\numberline {5.9.1}Type classes and sorts }{66}{subsection.5.9.1}} |
|
153 \newlabel{sec:types-pure}{{5.9.2}{67}{Types and type abbreviations \label {sec:types-pure}\relax }{subsection.5.9.2}{}} |
|
154 \@writefile{toc}{\contentsline {subsection}{\numberline {5.9.2}Types and type abbreviations }{67}{subsection.5.9.2}} |
|
155 \citation{nipkow-prehofer} |
|
156 \@writefile{toc}{\contentsline {subsection}{\numberline {5.9.3}Co-regularity of type classes and arities}{68}{subsection.5.9.3}} |
|
157 \newlabel{sec:consts}{{5.9.4}{68}{Constants and definitions \label {sec:consts}\relax }{subsection.5.9.4}{}} |
|
158 \@writefile{toc}{\contentsline {subsection}{\numberline {5.9.4}Constants and definitions }{68}{subsection.5.9.4}} |
|
159 \newlabel{sec:axms-thms}{{5.10}{71}{Axioms and theorems \label {sec:axms-thms}\relax }{section.5.10}{}} |
|
160 \@writefile{toc}{\contentsline {section}{\numberline {5.10}Axioms and theorems }{71}{section.5.10}} |
|
161 \@writefile{toc}{\contentsline {section}{\numberline {5.11}Oracles}{71}{section.5.11}} |
|
162 \@writefile{toc}{\contentsline {section}{\numberline {5.12}Name spaces}{72}{section.5.12}} |
|
163 \@writefile{toc}{\contentsline {chapter}{\numberline {6}Proofs }{74}{chapter.6}} |
|
164 \@writefile{lof}{\addvspace {10\p@ }} |
|
165 \@writefile{lot}{\addvspace {10\p@ }} |
|
166 \newlabel{ch:proofs}{{6}{74}{Proofs \label {ch:proofs}\relax }{chapter.6}{}} |
|
167 \@writefile{toc}{\contentsline {section}{\numberline {6.1}Proof structure}{74}{section.6.1}} |
|
168 \@writefile{toc}{\contentsline {subsection}{\numberline {6.1.1}Blocks}{74}{subsection.6.1.1}} |
|
169 \@writefile{toc}{\contentsline {subsection}{\numberline {6.1.2}Omitting proofs}{75}{subsection.6.1.2}} |
|
170 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Statements}{76}{section.6.2}} |
|
171 \newlabel{sec:proof-context}{{6.2.1}{76}{Context elements \label {sec:proof-context}\relax }{subsection.6.2.1}{}} |
|
172 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2.1}Context elements }{76}{subsection.6.2.1}} |
|
173 \newlabel{sec:term-abbrev}{{6.2.2}{77}{Term abbreviations \label {sec:term-abbrev}\relax }{subsection.6.2.2}{}} |
|
174 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2.2}Term abbreviations }{77}{subsection.6.2.2}} |
|
175 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2.3}Facts and forward chaining}{79}{subsection.6.2.3}} |
|
176 \newlabel{sec:goals}{{6.2.4}{80}{Goals \label {sec:goals}\relax }{subsection.6.2.4}{}} |
|
177 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2.4}Goals }{80}{subsection.6.2.4}} |
|
178 \@writefile{toc}{\contentsline {section}{\numberline {6.3}Refinement steps}{83}{section.6.3}} |
|
179 \newlabel{sec:proof-meth}{{6.3.1}{83}{Proof method expressions \label {sec:proof-meth}\relax }{subsection.6.3.1}{}} |
|
180 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3.1}Proof method expressions }{83}{subsection.6.3.1}} |
|
181 \newlabel{sec:proof-steps}{{6.3.2}{85}{Initial and terminal proof steps \label {sec:proof-steps}\relax }{subsection.6.3.2}{}} |
|
182 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3.2}Initial and terminal proof steps }{85}{subsection.6.3.2}} |
|
183 \newlabel{sec:pure-meth-att}{{6.3.3}{87}{Fundamental methods and attributes \label {sec:pure-meth-att}\relax }{subsection.6.3.3}{}} |
|
184 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3.3}Fundamental methods and attributes }{87}{subsection.6.3.3}} |
|
185 \newlabel{sec:tactic-commands}{{6.3.4}{89}{Emulating tactic scripts \label {sec:tactic-commands}\relax }{subsection.6.3.4}{}} |
|
186 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3.4}Emulating tactic scripts }{89}{subsection.6.3.4}} |
|
187 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3.5}Defining proof methods}{91}{subsection.6.3.5}} |
|
188 \newlabel{sec:obtain}{{6.4}{92}{Generalized elimination \label {sec:obtain}\relax }{section.6.4}{}} |
|
189 \@writefile{toc}{\contentsline {section}{\numberline {6.4}Generalized elimination }{92}{section.6.4}} |
|
190 \newlabel{sec:calculation}{{6.5}{93}{Calculational reasoning \label {sec:calculation}\relax }{section.6.5}{}} |
|
191 \@writefile{toc}{\contentsline {section}{\numberline {6.5}Calculational reasoning }{93}{section.6.5}} |
|
192 \newlabel{sec:cases-induct}{{6.6}{95}{Proof by cases and induction \label {sec:cases-induct}\relax }{section.6.6}{}} |
|
193 \@writefile{toc}{\contentsline {section}{\numberline {6.6}Proof by cases and induction }{95}{section.6.6}} |
|
194 \@writefile{toc}{\contentsline {subsection}{\numberline {6.6.1}Rule contexts}{95}{subsection.6.6.1}} |
|
195 \@writefile{toc}{\contentsline {subsection}{\numberline {6.6.2}Proof methods}{98}{subsection.6.6.2}} |
|
196 \@writefile{toc}{\contentsline {subsection}{\numberline {6.6.3}Declaring rules}{102}{subsection.6.6.3}} |
|
197 \@writefile{toc}{\contentsline {chapter}{\numberline {7}Inner syntax --- the term language }{104}{chapter.7}} |
|
198 \@writefile{lof}{\addvspace {10\p@ }} |
|
199 \@writefile{lot}{\addvspace {10\p@ }} |
|
200 \newlabel{ch:inner-syntax}{{7}{104}{Inner syntax --- the term language \label {ch:inner-syntax}\relax }{chapter.7}{}} |
|
201 \@writefile{toc}{\contentsline {section}{\numberline {7.1}Printing logical entities}{104}{section.7.1}} |
|
202 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Diagnostic commands}{104}{subsection.7.1.1}} |
|
203 \citation{isabelle-ref} |
|
204 \citation{isabelle-sys} |
|
205 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Details of printed content}{106}{subsection.7.1.2}} |
|
206 \@writefile{toc}{\contentsline {subsection}{\numberline {7.1.3}Printing limits}{108}{subsection.7.1.3}} |
|
207 \@writefile{toc}{\contentsline {section}{\numberline {7.2}Mixfix annotations}{108}{section.7.2}} |
|
208 \citation{paulson-ml2} |
|
209 \@writefile{toc}{\contentsline {section}{\numberline {7.3}Explicit term notation}{111}{section.7.3}} |
|
210 \newlabel{sec:pure-syntax}{{7.4}{111}{The Pure syntax \label {sec:pure-syntax}\relax }{section.7.4}{}} |
|
211 \@writefile{toc}{\contentsline {section}{\numberline {7.4}The Pure syntax }{111}{section.7.4}} |
|
212 \newlabel{sec:priority-grammar}{{7.4.1}{111}{Priority grammars \label {sec:priority-grammar}\relax }{subsection.7.4.1}{}} |
|
213 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.1}Priority grammars }{111}{subsection.7.4.1}} |
|
214 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.2}The Pure grammar}{113}{subsection.7.4.2}} |
|
215 \newlabel{sec:inner-lex}{{7.5}{116}{Lexical matters \label {sec:inner-lex}\relax }{section.7.5}{}} |
|
216 \@writefile{toc}{\contentsline {section}{\numberline {7.5}Lexical matters }{116}{section.7.5}} |
|
217 \newlabel{sec:syn-trans}{{7.6}{117}{Syntax and translations \label {sec:syn-trans}\relax }{section.7.6}{}} |
|
218 \@writefile{toc}{\contentsline {section}{\numberline {7.6}Syntax and translations }{117}{section.7.6}} |
|
219 \citation{isabelle-ref} |
|
220 \newlabel{sec:tr-funs}{{7.7}{119}{Syntax translation functions \label {sec:tr-funs}\relax }{section.7.7}{}} |
|
221 \@writefile{toc}{\contentsline {section}{\numberline {7.7}Syntax translation functions }{119}{section.7.7}} |
|
222 \@writefile{toc}{\contentsline {section}{\numberline {7.8}Inspecting the syntax}{120}{section.7.8}} |
|
223 \@writefile{toc}{\contentsline {chapter}{\numberline {8}Other commands}{122}{chapter.8}} |
|
224 \@writefile{lof}{\addvspace {10\p@ }} |
|
225 \@writefile{lot}{\addvspace {10\p@ }} |
|
226 \@writefile{toc}{\contentsline {section}{\numberline {8.1}Inspecting the context}{122}{section.8.1}} |
|
227 \citation{isabelle-sys} |
|
228 \newlabel{sec:history}{{8.2}{124}{History commands \label {sec:history}\relax }{section.8.2}{}} |
|
229 \@writefile{toc}{\contentsline {section}{\numberline {8.2}History commands }{124}{section.8.2}} |
30 \citation{proofgeneral} |
230 \citation{proofgeneral} |
31 \citation{Aspinall:TACAS:2000} |
231 \citation{Aspinall:TACAS:2000} |
32 \@writefile{toc}{\contentsline {section}{\numberline {1.2}User interfaces}{2}{section.1.2}} |
232 \@writefile{toc}{\contentsline {section}{\numberline {8.3}System commands}{125}{section.8.3}} |
33 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}Terminal sessions}{2}{subsection.1.2.1}} |
233 \@writefile{toc}{\contentsline {chapter}{\numberline {9}Generic tools and packages }{126}{chapter.9}} |
34 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}Emacs Proof General}{2}{subsection.1.2.2}} |
234 \@writefile{lof}{\addvspace {10\p@ }} |
35 \citation{proofgeneral} |
235 \@writefile{lot}{\addvspace {10\p@ }} |
36 \citation{isabelle-sys} |
236 \newlabel{ch:gen-tools}{{9}{126}{Generic tools and packages \label {ch:gen-tools}\relax }{chapter.9}{}} |
37 \citation{x-symbol} |
237 \@writefile{toc}{\contentsline {section}{\numberline {9.1}Configuration options}{126}{section.9.1}} |
38 \@writefile{toc}{\contentsline {subsubsection}{Proof\nobreakspace {}General as default Isabelle interface}{3}{section*.2}} |
238 \citation{isabelle-implementation} |
39 \@writefile{toc}{\contentsline {subsubsection}{The X-Symbol package}{4}{section*.3}} |
239 \@writefile{toc}{\contentsline {section}{\numberline {9.2}Basic proof tools}{127}{section.9.2}} |
40 \@writefile{toc}{\contentsline {section}{\numberline {1.3}Isabelle/Isar theories}{4}{section.1.3}} |
240 \newlabel{sec:misc-meth-att}{{9.2.1}{127}{Miscellaneous methods and attributes \label {sec:misc-meth-att}\relax }{subsection.9.2.1}{}} |
41 \citation{Wenzel:1999:TPHOL} |
241 \@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Miscellaneous methods and attributes }{127}{subsection.9.2.1}} |
42 \citation{Wiedijk:2000:MV} |
242 \citation{isabelle-implementation} |
43 \citation{Bauer-Wenzel:2000:HB} |
243 \@writefile{toc}{\contentsline {subsection}{\numberline {9.2.2}Low-level equational reasoning}{129}{subsection.9.2.2}} |
44 \citation{Bauer-Wenzel:2001} |
244 \newlabel{sec:tactics}{{9.2.3}{130}{Further tactic emulations \label {sec:tactics}\relax }{subsection.9.2.3}{}} |
45 \citation{Wenzel-PhD} |
245 \@writefile{toc}{\contentsline {subsection}{\numberline {9.2.3}Further tactic emulations }{130}{subsection.9.2.3}} |
46 \newlabel{sec:isar-howto}{{1.4}{5}{How to write Isar proofs anyway? \label {sec:isar-howto}\relax }{section.1.4}{}} |
246 \citation{isabelle-implementation} |
47 \@writefile{toc}{\contentsline {section}{\numberline {1.4}How to write Isar proofs anyway? }{5}{section.1.4}} |
247 \citation{isabelle-implementation} |
48 \citation{isabelle-sys} |
248 \citation{isabelle-implementation} |
49 \citation{proofgeneral} |
249 \citation{isabelle-implementation} |
50 \@writefile{toc}{\contentsline {chapter}{\numberline {2}Outer syntax}{6}{chapter.2}} |
250 \citation{isabelle-implementation} |
51 \@writefile{lof}{\addvspace {10\p@ }} |
251 \citation{isabelle-implementation} |
52 \@writefile{lot}{\addvspace {10\p@ }} |
252 \citation{isabelle-implementation} |
53 \citation{isabelle-ref} |
253 \newlabel{sec:simplifier}{{9.3}{133}{The Simplifier \label {sec:simplifier}\relax }{section.9.3}{}} |
54 \newlabel{sec:lex-syntax}{{2.1}{7}{Lexical matters \label {sec:lex-syntax}\relax }{section.2.1}{}} |
254 \@writefile{toc}{\contentsline {section}{\numberline {9.3}The Simplifier }{133}{section.9.3}} |
55 \@writefile{toc}{\contentsline {section}{\numberline {2.1}Lexical matters }{7}{section.2.1}} |
255 \@writefile{toc}{\contentsline {subsection}{\numberline {9.3.1}Simplification methods}{133}{subsection.9.3.1}} |
56 \citation{isabelle-sys} |
256 \citation{isabelle-ref} |
57 \@writefile{toc}{\contentsline {section}{\numberline {2.2}Common syntax entities}{8}{section.2.2}} |
257 \citation{isabelle-ref} |
58 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}Names}{8}{subsection.2.2.1}} |
258 \citation{isabelle-ref} |
59 \newlabel{sec:comments}{{2.2.2}{9}{Comments \label {sec:comments}\relax }{subsection.2.2.2}{}} |
259 \citation{isabelle-ref} |
60 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.2}Comments }{9}{subsection.2.2.2}} |
260 \@writefile{toc}{\contentsline {subsection}{\numberline {9.3.2}Declaring rules}{135}{subsection.9.3.2}} |
61 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.3}Type classes, sorts and arities}{9}{subsection.2.2.3}} |
261 \@writefile{toc}{\contentsline {subsection}{\numberline {9.3.3}Simplification procedures}{136}{subsection.9.3.3}} |
62 \newlabel{sec:types-terms}{{2.2.4}{10}{Types and terms \label {sec:types-terms}\relax }{subsection.2.2.4}{}} |
262 \citation{isabelle-ref} |
63 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.4}Types and terms }{10}{subsection.2.2.4}} |
263 \@writefile{toc}{\contentsline {subsection}{\numberline {9.3.4}Forward simplification}{137}{subsection.9.3.4}} |
64 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.5}Mixfix annotations}{11}{subsection.2.2.5}} |
264 \newlabel{sec:classical}{{9.4}{137}{The Classical Reasoner \label {sec:classical}\relax }{section.9.4}{}} |
65 \citation{isabelle-ref} |
265 \@writefile{toc}{\contentsline {section}{\numberline {9.4}The Classical Reasoner }{137}{section.9.4}} |
66 \newlabel{sec:syn-meth}{{2.2.6}{12}{Proof methods \label {sec:syn-meth}\relax }{subsection.2.2.6}{}} |
266 \@writefile{toc}{\contentsline {subsection}{\numberline {9.4.1}Basic methods}{137}{subsection.9.4.1}} |
67 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.6}Proof methods }{12}{subsection.2.2.6}} |
267 \@writefile{toc}{\contentsline {subsection}{\numberline {9.4.2}Automated methods}{138}{subsection.9.4.2}} |
68 \newlabel{sec:syn-att}{{2.2.7}{14}{Attributes and theorems \label {sec:syn-att}\relax }{subsection.2.2.7}{}} |
268 \citation{isabelle-ref} |
69 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.7}Attributes and theorems }{14}{subsection.2.2.7}} |
269 \citation{isabelle-ref} |
70 \newlabel{sec:term-decls}{{2.2.8}{16}{Term patterns and declarations \label {sec:term-decls}\relax }{subsection.2.2.8}{}} |
270 \newlabel{sec:clasimp}{{9.4.3}{139}{Combined automated methods \label {sec:clasimp}\relax }{subsection.9.4.3}{}} |
71 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2.8}Term patterns and declarations }{16}{subsection.2.2.8}} |
271 \@writefile{toc}{\contentsline {subsection}{\numberline {9.4.3}Combined automated methods }{139}{subsection.9.4.3}} |
72 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Theory specifications}{18}{chapter.3}} |
272 \citation{isabelle-ref} |
73 \@writefile{lof}{\addvspace {10\p@ }} |
273 \citation{isabelle-ref} |
74 \@writefile{lot}{\addvspace {10\p@ }} |
274 \@writefile{toc}{\contentsline {subsection}{\numberline {9.4.4}Declaring rules}{141}{subsection.9.4.4}} |
75 \newlabel{sec:begin-thy}{{3.1}{18}{Defining theories \label {sec:begin-thy}\relax }{section.3.1}{}} |
275 \@writefile{toc}{\contentsline {subsection}{\numberline {9.4.5}Classical operations}{142}{subsection.9.4.5}} |
76 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Defining theories }{18}{section.3.1}} |
276 \newlabel{sec:object-logic}{{9.5}{142}{Object-logic setup \label {sec:object-logic}\relax }{section.9.5}{}} |
77 \newlabel{sec:target}{{3.2}{19}{Local theory targets \label {sec:target}\relax }{section.3.2}{}} |
277 \@writefile{toc}{\contentsline {section}{\numberline {9.5}Object-logic setup }{142}{section.9.5}} |
78 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Local theory targets }{19}{section.3.2}} |
278 \@writefile{toc}{\contentsline {part}{III\hspace {1em}Object-Logics}{144}{part.3}} |
79 \@writefile{toc}{\contentsline {section}{\numberline {3.3}Basic specification elements}{20}{section.3.3}} |
279 \@writefile{toc}{\contentsline {chapter}{\numberline {10}Isabelle/HOL }{145}{chapter.10}} |
80 \@writefile{toc}{\contentsline {section}{\numberline {3.4}Generic declarations}{22}{section.3.4}} |
280 \@writefile{lof}{\addvspace {10\p@ }} |
81 \newlabel{sec:locale}{{3.5}{23}{Locales \label {sec:locale}\relax }{section.3.5}{}} |
281 \@writefile{lot}{\addvspace {10\p@ }} |
82 \@writefile{toc}{\contentsline {section}{\numberline {3.5}Locales }{23}{section.3.5}} |
282 \newlabel{ch:hol}{{10}{145}{Isabelle/HOL \label {ch:hol}\relax }{chapter.10}{}} |
83 \@writefile{toc}{\contentsline {subsection}{\numberline {3.5.1}Locale specifications}{23}{subsection.3.5.1}} |
283 \newlabel{sec:hol-typedef}{{10.1}{145}{Primitive types \label {sec:hol-typedef}\relax }{section.10.1}{}} |
84 \@writefile{toc}{\contentsline {subsection}{\numberline {3.5.2}Interpretation of locales}{27}{subsection.3.5.2}} |
284 \@writefile{toc}{\contentsline {section}{\numberline {10.1}Primitive types }{145}{section.10.1}} |
85 \citation{Wenzel:1997:TPHOL} |
285 \@writefile{toc}{\contentsline {section}{\numberline {10.2}Adhoc tuples}{146}{section.10.2}} |
86 \citation{isabelle-classes} |
286 \citation{NaraschewskiW-TPHOLs98} |
87 \newlabel{sec:class}{{3.6}{30}{Classes \label {sec:class}\relax }{section.3.6}{}} |
287 \newlabel{sec:hol-record}{{10.3}{147}{Records \label {sec:hol-record}\relax }{section.10.3}{}} |
88 \@writefile{toc}{\contentsline {section}{\numberline {3.6}Classes }{30}{section.3.6}} |
288 \@writefile{toc}{\contentsline {section}{\numberline {10.3}Records }{147}{section.10.3}} |
89 \@writefile{toc}{\contentsline {subsection}{\numberline {3.6.1}The class target}{33}{subsection.3.6.1}} |
289 \@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Basic concepts}{147}{subsection.10.3.1}} |
90 \newlabel{sec:axclass}{{3.6.2}{33}{Old-style axiomatic type classes \label {sec:axclass}\relax }{subsection.3.6.2}{}} |
|
91 \@writefile{toc}{\contentsline {subsection}{\numberline {3.6.2}Old-style axiomatic type classes }{33}{subsection.3.6.2}} |
|
92 \@writefile{toc}{\contentsline {section}{\numberline {3.7}Unrestricted overloading}{34}{section.3.7}} |
|
93 \newlabel{sec:ML}{{3.8}{35}{Incorporating ML code \label {sec:ML}\relax }{section.3.8}{}} |
|
94 \@writefile{toc}{\contentsline {section}{\numberline {3.8}Incorporating ML code }{35}{section.3.8}} |
|
95 \@writefile{toc}{\contentsline {section}{\numberline {3.9}Primitive specification elements}{36}{section.3.9}} |
|
96 \newlabel{sec:classes}{{3.9.1}{36}{Type classes and sorts \label {sec:classes}\relax }{subsection.3.9.1}{}} |
|
97 \@writefile{toc}{\contentsline {subsection}{\numberline {3.9.1}Type classes and sorts }{36}{subsection.3.9.1}} |
|
98 \citation{isabelle-sys} |
|
99 \newlabel{sec:types-pure}{{3.9.2}{37}{Types and type abbreviations \label {sec:types-pure}\relax }{subsection.3.9.2}{}} |
|
100 \@writefile{toc}{\contentsline {subsection}{\numberline {3.9.2}Types and type abbreviations }{37}{subsection.3.9.2}} |
|
101 \newlabel{sec:consts}{{3.9.3}{38}{Constants and definitions \label {sec:consts}\relax }{subsection.3.9.3}{}} |
|
102 \@writefile{toc}{\contentsline {subsection}{\numberline {3.9.3}Constants and definitions }{38}{subsection.3.9.3}} |
|
103 \newlabel{sec:axms-thms}{{3.10}{41}{Axioms and theorems \label {sec:axms-thms}\relax }{section.3.10}{}} |
|
104 \@writefile{toc}{\contentsline {section}{\numberline {3.10}Axioms and theorems }{41}{section.3.10}} |
|
105 \@writefile{toc}{\contentsline {section}{\numberline {3.11}Oracles}{42}{section.3.11}} |
|
106 \@writefile{toc}{\contentsline {section}{\numberline {3.12}Name spaces}{42}{section.3.12}} |
|
107 \newlabel{sec:syn-trans}{{3.13}{43}{Syntax and translations \label {sec:syn-trans}\relax }{section.3.13}{}} |
|
108 \@writefile{toc}{\contentsline {section}{\numberline {3.13}Syntax and translations }{43}{section.3.13}} |
|
109 \@writefile{toc}{\contentsline {section}{\numberline {3.14}Syntax translation functions}{44}{section.3.14}} |
|
110 \citation{isabelle-ref} |
|
111 \@writefile{toc}{\contentsline {chapter}{\numberline {4}Proofs}{46}{chapter.4}} |
|
112 \@writefile{lof}{\addvspace {10\p@ }} |
|
113 \@writefile{lot}{\addvspace {10\p@ }} |
|
114 \newlabel{sec:proof-context}{{4.1}{46}{Context elements \label {sec:proof-context}\relax }{section.4.1}{}} |
|
115 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Context elements }{46}{section.4.1}} |
|
116 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Facts and forward chaining}{48}{section.4.2}} |
|
117 \newlabel{sec:goals}{{4.3}{50}{Goal statements \label {sec:goals}\relax }{section.4.3}{}} |
|
118 \@writefile{toc}{\contentsline {section}{\numberline {4.3}Goal statements }{50}{section.4.3}} |
|
119 \newlabel{sec:proof-steps}{{4.4}{53}{Initial and terminal proof steps \label {sec:proof-steps}\relax }{section.4.4}{}} |
|
120 \@writefile{toc}{\contentsline {section}{\numberline {4.4}Initial and terminal proof steps }{53}{section.4.4}} |
|
121 \newlabel{sec:pure-meth-att}{{4.5}{55}{Fundamental methods and attributes \label {sec:pure-meth-att}\relax }{section.4.5}{}} |
|
122 \@writefile{toc}{\contentsline {section}{\numberline {4.5}Fundamental methods and attributes }{55}{section.4.5}} |
|
123 \newlabel{sec:term-abbrev}{{4.6}{58}{Term abbreviations \label {sec:term-abbrev}\relax }{section.4.6}{}} |
|
124 \@writefile{toc}{\contentsline {section}{\numberline {4.6}Term abbreviations }{58}{section.4.6}} |
|
125 \@writefile{toc}{\contentsline {section}{\numberline {4.7}Block structure}{59}{section.4.7}} |
|
126 \newlabel{sec:tactic-commands}{{4.8}{60}{Emulating tactic scripts \label {sec:tactic-commands}\relax }{section.4.8}{}} |
|
127 \@writefile{toc}{\contentsline {section}{\numberline {4.8}Emulating tactic scripts }{60}{section.4.8}} |
|
128 \citation{isabelle-sys} |
|
129 \@writefile{toc}{\contentsline {section}{\numberline {4.9}Omitting proofs}{61}{section.4.9}} |
|
130 \newlabel{sec:obtain}{{4.10}{62}{Generalized elimination \label {sec:obtain}\relax }{section.4.10}{}} |
|
131 \@writefile{toc}{\contentsline {section}{\numberline {4.10}Generalized elimination }{62}{section.4.10}} |
|
132 \newlabel{sec:calculation}{{4.11}{64}{Calculational reasoning \label {sec:calculation}\relax }{section.4.11}{}} |
|
133 \@writefile{toc}{\contentsline {section}{\numberline {4.11}Calculational reasoning }{64}{section.4.11}} |
|
134 \newlabel{sec:cases-induct}{{4.12}{66}{Proof by cases and induction \label {sec:cases-induct}\relax }{section.4.12}{}} |
|
135 \@writefile{toc}{\contentsline {section}{\numberline {4.12}Proof by cases and induction }{66}{section.4.12}} |
|
136 \@writefile{toc}{\contentsline {subsection}{\numberline {4.12.1}Rule contexts}{66}{subsection.4.12.1}} |
|
137 \@writefile{toc}{\contentsline {subsection}{\numberline {4.12.2}Proof methods}{68}{subsection.4.12.2}} |
|
138 \@writefile{toc}{\contentsline {subsection}{\numberline {4.12.3}Declaring rules}{72}{subsection.4.12.3}} |
|
139 \citation{isabelle-sys} |
|
140 \citation{isabelle-sys} |
|
141 \citation{isabelle-hol-book} |
290 \citation{isabelle-hol-book} |
142 \@writefile{toc}{\contentsline {chapter}{\numberline {5}Document preparation }{74}{chapter.5}} |
291 \@writefile{toc}{\contentsline {subsection}{\numberline {10.3.2}Record specifications}{148}{subsection.10.3.2}} |
143 \@writefile{lof}{\addvspace {10\p@ }} |
292 \@writefile{toc}{\contentsline {subsection}{\numberline {10.3.3}Record operations}{149}{subsection.10.3.3}} |
144 \@writefile{lot}{\addvspace {10\p@ }} |
293 \@writefile{toc}{\contentsline {subsection}{\numberline {10.3.4}Derived rules and proof tools}{150}{subsection.10.3.4}} |
145 \newlabel{ch:document-prep}{{5}{74}{Document preparation \label {ch:document-prep}\relax }{chapter.5}{}} |
|
146 \citation{isabelle-sys} |
|
147 \newlabel{sec:markup}{{5.1}{75}{Markup commands \label {sec:markup}\relax }{section.5.1}{}} |
|
148 \@writefile{toc}{\contentsline {section}{\numberline {5.1}Markup commands }{75}{section.5.1}} |
|
149 \newlabel{sec:antiq}{{5.2}{77}{Antiquotations \label {sec:antiq}\relax }{section.5.2}{}} |
|
150 \@writefile{toc}{\contentsline {section}{\numberline {5.2}Antiquotations }{77}{section.5.2}} |
|
151 \citation{isabelle-ref} |
|
152 \citation{isabelle-ref} |
|
153 \citation{isabelle-sys} |
|
154 \newlabel{sec:tags}{{5.3}{82}{Tagged commands \label {sec:tags}\relax }{section.5.3}{}} |
|
155 \@writefile{toc}{\contentsline {section}{\numberline {5.3}Tagged commands }{82}{section.5.3}} |
|
156 \@writefile{toc}{\contentsline {section}{\numberline {5.4}Draft presentation}{82}{section.5.4}} |
|
157 \@writefile{toc}{\contentsline {chapter}{\numberline {6}Other commands }{84}{chapter.6}} |
|
158 \@writefile{lof}{\addvspace {10\p@ }} |
|
159 \@writefile{lot}{\addvspace {10\p@ }} |
|
160 \newlabel{ch:pure-syntax}{{6}{84}{Other commands \label {ch:pure-syntax}\relax }{chapter.6}{}} |
|
161 \@writefile{toc}{\contentsline {section}{\numberline {6.1}Diagnostics}{84}{section.6.1}} |
|
162 \citation{isabelle-ref} |
|
163 \citation{isabelle-sys} |
|
164 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Inspecting the context}{86}{section.6.2}} |
|
165 \citation{isabelle-ref} |
|
166 \citation{isabelle-sys} |
|
167 \citation{proofgeneral} |
|
168 \citation{Aspinall:TACAS:2000} |
|
169 \newlabel{sec:history}{{6.3}{88}{History commands \label {sec:history}\relax }{section.6.3}{}} |
|
170 \@writefile{toc}{\contentsline {section}{\numberline {6.3}History commands }{88}{section.6.3}} |
|
171 \@writefile{toc}{\contentsline {section}{\numberline {6.4}System commands}{89}{section.6.4}} |
|
172 \@writefile{toc}{\contentsline {chapter}{\numberline {7}Generic tools and packages }{90}{chapter.7}} |
|
173 \@writefile{lof}{\addvspace {10\p@ }} |
|
174 \@writefile{lot}{\addvspace {10\p@ }} |
|
175 \newlabel{ch:gen-tools}{{7}{90}{Generic tools and packages \label {ch:gen-tools}\relax }{chapter.7}{}} |
|
176 \@writefile{toc}{\contentsline {section}{\numberline {7.1}Configuration options}{90}{section.7.1}} |
|
177 \citation{isabelle-ref} |
|
178 \@writefile{toc}{\contentsline {section}{\numberline {7.2}Basic proof tools}{91}{section.7.2}} |
|
179 \newlabel{sec:misc-meth-att}{{7.2.1}{91}{Miscellaneous methods and attributes \label {sec:misc-meth-att}\relax }{subsection.7.2.1}{}} |
|
180 \@writefile{toc}{\contentsline {subsection}{\numberline {7.2.1}Miscellaneous methods and attributes }{91}{subsection.7.2.1}} |
|
181 \citation{isabelle-ref} |
|
182 \@writefile{toc}{\contentsline {subsection}{\numberline {7.2.2}Low-level equational reasoning}{93}{subsection.7.2.2}} |
|
183 \newlabel{sec:tactics}{{7.2.3}{94}{Further tactic emulations \label {sec:tactics}\relax }{subsection.7.2.3}{}} |
|
184 \@writefile{toc}{\contentsline {subsection}{\numberline {7.2.3}Further tactic emulations }{94}{subsection.7.2.3}} |
|
185 \citation{isabelle-ref} |
|
186 \citation{isabelle-ref} |
|
187 \citation{isabelle-ref} |
|
188 \citation{isabelle-ref} |
|
189 \citation{isabelle-ref} |
|
190 \citation{isabelle-ref} |
|
191 \citation{isabelle-ref} |
|
192 \newlabel{sec:simplifier}{{7.3}{97}{The Simplifier \label {sec:simplifier}\relax }{section.7.3}{}} |
|
193 \@writefile{toc}{\contentsline {section}{\numberline {7.3}The Simplifier }{97}{section.7.3}} |
|
194 \@writefile{toc}{\contentsline {subsection}{\numberline {7.3.1}Simplification methods}{97}{subsection.7.3.1}} |
|
195 \citation{isabelle-ref} |
|
196 \citation{isabelle-ref} |
|
197 \citation{isabelle-ref} |
|
198 \citation{isabelle-ref} |
|
199 \@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}Declaring rules}{99}{subsection.7.3.2}} |
|
200 \@writefile{toc}{\contentsline {subsection}{\numberline {7.3.3}Simplification procedures}{100}{subsection.7.3.3}} |
|
201 \citation{isabelle-ref} |
|
202 \@writefile{toc}{\contentsline {subsection}{\numberline {7.3.4}Forward simplification}{101}{subsection.7.3.4}} |
|
203 \newlabel{sec:classical}{{7.4}{101}{The Classical Reasoner \label {sec:classical}\relax }{section.7.4}{}} |
|
204 \@writefile{toc}{\contentsline {section}{\numberline {7.4}The Classical Reasoner }{101}{section.7.4}} |
|
205 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.1}Basic methods}{101}{subsection.7.4.1}} |
|
206 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.2}Automated methods}{102}{subsection.7.4.2}} |
|
207 \citation{isabelle-ref} |
|
208 \citation{isabelle-ref} |
|
209 \newlabel{sec:clasimp}{{7.4.3}{103}{Combined automated methods \label {sec:clasimp}\relax }{subsection.7.4.3}{}} |
|
210 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.3}Combined automated methods }{103}{subsection.7.4.3}} |
|
211 \citation{isabelle-ref} |
|
212 \citation{isabelle-ref} |
|
213 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.4}Declaring rules}{105}{subsection.7.4.4}} |
|
214 \@writefile{toc}{\contentsline {subsection}{\numberline {7.4.5}Classical operations}{106}{subsection.7.4.5}} |
|
215 \newlabel{sec:object-logic}{{7.5}{106}{Object-logic setup \label {sec:object-logic}\relax }{section.7.5}{}} |
|
216 \@writefile{toc}{\contentsline {section}{\numberline {7.5}Object-logic setup }{106}{section.7.5}} |
|
217 \@writefile{toc}{\contentsline {chapter}{\numberline {8}Isabelle/HOL }{108}{chapter.8}} |
|
218 \@writefile{lof}{\addvspace {10\p@ }} |
|
219 \@writefile{lot}{\addvspace {10\p@ }} |
|
220 \newlabel{ch:hol}{{8}{108}{Isabelle/HOL \label {ch:hol}\relax }{chapter.8}{}} |
|
221 \newlabel{sec:hol-typedef}{{8.1}{108}{Primitive types \label {sec:hol-typedef}\relax }{section.8.1}{}} |
|
222 \@writefile{toc}{\contentsline {section}{\numberline {8.1}Primitive types }{108}{section.8.1}} |
|
223 \@writefile{toc}{\contentsline {section}{\numberline {8.2}Adhoc tuples}{109}{section.8.2}} |
|
224 \citation{NaraschewskiW-TPHOLs98} |
|
225 \newlabel{sec:hol-record}{{8.3}{110}{Records \label {sec:hol-record}\relax }{section.8.3}{}} |
|
226 \@writefile{toc}{\contentsline {section}{\numberline {8.3}Records }{110}{section.8.3}} |
|
227 \@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Basic concepts}{110}{subsection.8.3.1}} |
|
228 \citation{isabelle-hol-book} |
|
229 \@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Record specifications}{111}{subsection.8.3.2}} |
|
230 \@writefile{toc}{\contentsline {subsection}{\numberline {8.3.3}Record operations}{112}{subsection.8.3.3}} |
|
231 \@writefile{toc}{\contentsline {subsection}{\numberline {8.3.4}Derived rules and proof tools}{113}{subsection.8.3.4}} |
|
232 \citation{isabelle-HOL} |
294 \citation{isabelle-HOL} |
233 \newlabel{sec:hol-datatype}{{8.4}{114}{Datatypes \label {sec:hol-datatype}\relax }{section.8.4}{}} |
295 \newlabel{sec:hol-datatype}{{10.4}{151}{Datatypes \label {sec:hol-datatype}\relax }{section.10.4}{}} |
234 \@writefile{toc}{\contentsline {section}{\numberline {8.4}Datatypes }{114}{section.8.4}} |
296 \@writefile{toc}{\contentsline {section}{\numberline {10.4}Datatypes }{151}{section.10.4}} |
235 \newlabel{sec:recursion}{{8.5}{115}{Recursive functions \label {sec:recursion}\relax }{section.8.5}{}} |
297 \newlabel{sec:recursion}{{10.5}{152}{Recursive functions \label {sec:recursion}\relax }{section.10.5}{}} |
236 \@writefile{toc}{\contentsline {section}{\numberline {8.5}Recursive functions }{115}{section.8.5}} |
298 \@writefile{toc}{\contentsline {section}{\numberline {10.5}Recursive functions }{152}{section.10.5}} |
237 \citation{isabelle-HOL} |
299 \citation{isabelle-HOL} |
238 \citation{isabelle-function} |
300 \citation{isabelle-function} |
239 \citation{isabelle-function} |
301 \citation{isabelle-function} |
240 \citation{isabelle-function} |
302 \citation{isabelle-function} |
241 \citation{isabelle-function} |
303 \citation{isabelle-function} |
242 \@writefile{toc}{\contentsline {subsection}{\numberline {8.5.1}Proof methods related to recursive definitions}{117}{subsection.8.5.1}} |
304 \@writefile{toc}{\contentsline {subsection}{\numberline {10.5.1}Proof methods related to recursive definitions}{154}{subsection.10.5.1}} |
243 \citation{isabelle-HOL} |
305 \citation{isabelle-HOL} |
244 \@writefile{toc}{\contentsline {subsection}{\numberline {8.5.2}Old-style recursive function definitions (TFL)}{118}{subsection.8.5.2}} |
306 \@writefile{toc}{\contentsline {subsection}{\numberline {10.5.2}Old-style recursive function definitions (TFL)}{155}{subsection.10.5.2}} |
245 \citation{paulson-CADE} |
307 \citation{paulson-CADE} |
246 \newlabel{sec:hol-inductive}{{8.6}{119}{Inductive and coinductive definitions \label {sec:hol-inductive}\relax }{section.8.6}{}} |
308 \newlabel{sec:hol-inductive}{{10.6}{156}{Inductive and coinductive definitions \label {sec:hol-inductive}\relax }{section.10.6}{}} |
247 \@writefile{toc}{\contentsline {section}{\numberline {8.6}Inductive and coinductive definitions }{119}{section.8.6}} |
309 \@writefile{toc}{\contentsline {section}{\numberline {10.6}Inductive and coinductive definitions }{156}{section.10.6}} |
248 \@writefile{toc}{\contentsline {subsection}{\numberline {8.6.1}Derived rules}{121}{subsection.8.6.1}} |
310 \@writefile{toc}{\contentsline {subsection}{\numberline {10.6.1}Derived rules}{158}{subsection.10.6.1}} |
249 \@writefile{toc}{\contentsline {subsection}{\numberline {8.6.2}Monotonicity theorems}{121}{subsection.8.6.2}} |
311 \@writefile{toc}{\contentsline {subsection}{\numberline {10.6.2}Monotonicity theorems}{158}{subsection.10.6.2}} |
250 \@writefile{toc}{\contentsline {section}{\numberline {8.7}Arithmetic proof support}{122}{section.8.7}} |
312 \@writefile{toc}{\contentsline {section}{\numberline {10.7}Arithmetic proof support}{159}{section.10.7}} |
251 \@writefile{toc}{\contentsline {section}{\numberline {8.8}Invoking automated reasoning tools -- The Sledgehammer}{122}{section.8.8}} |
313 \@writefile{toc}{\contentsline {section}{\numberline {10.8}Intuitionistic proof search}{159}{section.10.8}} |
252 \newlabel{sec:hol-induct-tac}{{8.9}{124}{Unstructured cases analysis and induction \label {sec:hol-induct-tac}\relax }{section.8.9}{}} |
314 \citation{Bezem-Coquand:2005} |
253 \@writefile{toc}{\contentsline {section}{\numberline {8.9}Unstructured cases analysis and induction }{124}{section.8.9}} |
315 \@writefile{toc}{\contentsline {section}{\numberline {10.9}Coherent Logic}{160}{section.10.9}} |
|
316 \@writefile{toc}{\contentsline {section}{\numberline {10.10}Checking and refuting propositions}{160}{section.10.10}} |
|
317 \citation{isabelle-ref} |
|
318 \@writefile{toc}{\contentsline {section}{\numberline {10.11}Invoking automated reasoning tools -- The Sledgehammer}{162}{section.10.11}} |
|
319 \newlabel{sec:hol-induct-tac}{{10.12}{163}{Unstructured case analysis and induction \label {sec:hol-induct-tac}\relax }{section.10.12}{}} |
|
320 \@writefile{toc}{\contentsline {section}{\numberline {10.12}Unstructured case analysis and induction }{163}{section.10.12}} |
254 \citation{isabelle-HOL} |
321 \citation{isabelle-HOL} |
255 \@writefile{toc}{\contentsline {section}{\numberline {8.10}Executable code}{125}{section.8.10}} |
322 \@writefile{toc}{\contentsline {section}{\numberline {10.13}Executable code}{165}{section.10.13}} |
256 \citation{SML} |
323 \citation{SML} |
257 \citation{OCaml} |
324 \citation{OCaml} |
258 \citation{haskell-revised-report} |
325 \citation{haskell-revised-report} |
259 \citation{isabelle-codegen} |
326 \citation{isabelle-codegen} |
260 \newlabel{sec:hol-specification}{{8.11}{133}{Definition by specification \label {sec:hol-specification}\relax }{section.8.11}{}} |
327 \newlabel{sec:hol-specification}{{10.14}{174}{Definition by specification \label {sec:hol-specification}\relax }{section.10.14}{}} |
261 \@writefile{toc}{\contentsline {section}{\numberline {8.11}Definition by specification }{133}{section.8.11}} |
328 \@writefile{toc}{\contentsline {section}{\numberline {10.14}Definition by specification }{174}{section.10.14}} |
262 \@writefile{toc}{\contentsline {chapter}{\numberline {9}Isabelle/HOLCF }{135}{chapter.9}} |
329 \@writefile{toc}{\contentsline {chapter}{\numberline {11}Isabelle/HOLCF }{176}{chapter.11}} |
263 \@writefile{lof}{\addvspace {10\p@ }} |
330 \@writefile{lof}{\addvspace {10\p@ }} |
264 \@writefile{lot}{\addvspace {10\p@ }} |
331 \@writefile{lot}{\addvspace {10\p@ }} |
265 \newlabel{ch:holcf}{{9}{135}{Isabelle/HOLCF \label {ch:holcf}\relax }{chapter.9}{}} |
332 \newlabel{ch:holcf}{{11}{176}{Isabelle/HOLCF \label {ch:holcf}\relax }{chapter.11}{}} |
266 \@writefile{toc}{\contentsline {section}{\numberline {9.1}Mixfix syntax for continuous operations}{135}{section.9.1}} |
333 \@writefile{toc}{\contentsline {section}{\numberline {11.1}Mixfix syntax for continuous operations}{176}{section.11.1}} |
267 \@writefile{toc}{\contentsline {section}{\numberline {9.2}Recursive domains}{135}{section.9.2}} |
334 \@writefile{toc}{\contentsline {section}{\numberline {11.2}Recursive domains}{176}{section.11.2}} |
268 \citation{MuellerNvOS99} |
335 \citation{MuellerNvOS99} |
269 \@writefile{toc}{\contentsline {chapter}{\numberline {10}Isabelle/ZF }{137}{chapter.10}} |
336 \@writefile{toc}{\contentsline {chapter}{\numberline {12}Isabelle/ZF }{178}{chapter.12}} |
270 \@writefile{lof}{\addvspace {10\p@ }} |
337 \@writefile{lof}{\addvspace {10\p@ }} |
271 \@writefile{lot}{\addvspace {10\p@ }} |
338 \@writefile{lot}{\addvspace {10\p@ }} |
272 \newlabel{ch:zf}{{10}{137}{Isabelle/ZF \label {ch:zf}\relax }{chapter.10}{}} |
339 \newlabel{ch:zf}{{12}{178}{Isabelle/ZF \label {ch:zf}\relax }{chapter.12}{}} |
273 \@writefile{toc}{\contentsline {section}{\numberline {10.1}Type checking}{137}{section.10.1}} |
340 \@writefile{toc}{\contentsline {section}{\numberline {12.1}Type checking}{178}{section.12.1}} |
274 \@writefile{toc}{\contentsline {section}{\numberline {10.2}(Co)Inductive sets and datatypes}{137}{section.10.2}} |
341 \@writefile{toc}{\contentsline {section}{\numberline {12.2}(Co)Inductive sets and datatypes}{178}{section.12.2}} |
275 \@writefile{toc}{\contentsline {subsection}{\numberline {10.2.1}Set definitions}{137}{subsection.10.2.1}} |
342 \@writefile{toc}{\contentsline {subsection}{\numberline {12.2.1}Set definitions}{178}{subsection.12.2.1}} |
276 \citation{isabelle-ZF} |
343 \citation{isabelle-ZF} |
277 \@writefile{toc}{\contentsline {subsection}{\numberline {10.2.2}Primitive recursive functions}{139}{subsection.10.2.2}} |
344 \@writefile{toc}{\contentsline {subsection}{\numberline {12.2.2}Primitive recursive functions}{180}{subsection.12.2.2}} |
278 \@writefile{toc}{\contentsline {subsection}{\numberline {10.2.3}Cases and induction: emulating tactic scripts}{140}{subsection.10.2.3}} |
345 \@writefile{toc}{\contentsline {subsection}{\numberline {12.2.3}Cases and induction: emulating tactic scripts}{181}{subsection.12.2.3}} |
279 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Isabelle/Isar quick reference }{141}{appendix.A}} |
346 \@writefile{toc}{\contentsline {part}{IV\hspace {1em}Appendix}{182}{part.4}} |
280 \@writefile{lof}{\addvspace {10\p@ }} |
347 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Isabelle/Isar quick reference }{183}{appendix.A}} |
281 \@writefile{lot}{\addvspace {10\p@ }} |
348 \@writefile{lof}{\addvspace {10\p@ }} |
282 \newlabel{ap:refcard}{{A}{141}{Isabelle/Isar quick reference \label {ap:refcard}\relax }{appendix.A}{}} |
349 \@writefile{lot}{\addvspace {10\p@ }} |
283 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Proof commands}{141}{section.A.1}} |
350 \newlabel{ap:refcard}{{A}{183}{Isabelle/Isar quick reference \label {ap:refcard}\relax }{appendix.A}{}} |
284 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.1}Primitives and basic syntax}{141}{subsection.A.1.1}} |
351 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Proof commands}{183}{section.A.1}} |
285 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.2}Abbreviations and synonyms}{142}{subsection.A.1.2}} |
352 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.1}Primitives and basic syntax}{183}{subsection.A.1.1}} |
286 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.3}Derived elements}{142}{subsection.A.1.3}} |
353 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.2}Abbreviations and synonyms}{184}{subsection.A.1.2}} |
287 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.4}Diagnostic commands}{142}{subsection.A.1.4}} |
354 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.3}Derived elements}{184}{subsection.A.1.3}} |
288 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Proof methods}{143}{section.A.2}} |
355 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1.4}Diagnostic commands}{184}{subsection.A.1.4}} |
289 \@writefile{toc}{\contentsline {section}{\numberline {A.3}Attributes}{144}{section.A.3}} |
356 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Proof methods}{185}{section.A.2}} |
290 \@writefile{toc}{\contentsline {section}{\numberline {A.4}Rule declarations and methods}{144}{section.A.4}} |
357 \@writefile{toc}{\contentsline {section}{\numberline {A.3}Attributes}{186}{section.A.3}} |
291 \@writefile{toc}{\contentsline {section}{\numberline {A.5}Emulating tactic scripts}{145}{section.A.5}} |
358 \@writefile{toc}{\contentsline {section}{\numberline {A.4}Rule declarations and methods}{186}{section.A.4}} |
292 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5.1}Commands}{145}{subsection.A.5.1}} |
359 \@writefile{toc}{\contentsline {section}{\numberline {A.5}Emulating tactic scripts}{187}{section.A.5}} |
293 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5.2}Methods}{145}{subsection.A.5.2}} |
360 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5.1}Commands}{187}{subsection.A.5.1}} |
294 \@writefile{toc}{\contentsline {chapter}{\numberline {B}ML tactic expressions}{146}{appendix.B}} |
361 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5.2}Methods}{187}{subsection.A.5.2}} |
295 \@writefile{lof}{\addvspace {10\p@ }} |
362 \@writefile{toc}{\contentsline {chapter}{\numberline {B}Predefined Isabelle symbols }{188}{appendix.B}} |
296 \@writefile{lot}{\addvspace {10\p@ }} |
363 \@writefile{lof}{\addvspace {10\p@ }} |
297 \@writefile{toc}{\contentsline {section}{\numberline {B.1}Resolution tactics}{146}{section.B.1}} |
364 \@writefile{lot}{\addvspace {10\p@ }} |
298 \citation{isabelle-ref} |
365 \newlabel{app:symbols}{{B}{188}{Predefined Isabelle symbols \label {app:symbols}\relax }{appendix.B}{}} |
299 \citation{isabelle-ref} |
366 \@writefile{toc}{\contentsline {chapter}{\numberline {C}ML tactic expressions}{194}{appendix.C}} |
300 \@writefile{toc}{\contentsline {section}{\numberline {B.2}Simplifier tactics}{147}{section.B.2}} |
367 \@writefile{lof}{\addvspace {10\p@ }} |
301 \@writefile{toc}{\contentsline {section}{\numberline {B.3}Classical Reasoner tactics}{147}{section.B.3}} |
368 \@writefile{lot}{\addvspace {10\p@ }} |
302 \@writefile{toc}{\contentsline {section}{\numberline {B.4}Miscellaneous tactics}{147}{section.B.4}} |
369 \@writefile{toc}{\contentsline {section}{\numberline {C.1}Resolution tactics}{194}{section.C.1}} |
303 \citation{isabelle-ref} |
370 \citation{isabelle-ref} |
304 \citation{isabelle-ref} |
371 \citation{isabelle-ref} |
305 \bibstyle{plain} |
372 \@writefile{toc}{\contentsline {section}{\numberline {C.2}Simplifier tactics}{195}{section.C.2}} |
|
373 \@writefile{toc}{\contentsline {section}{\numberline {C.3}Classical Reasoner tactics}{195}{section.C.3}} |
|
374 \@writefile{toc}{\contentsline {section}{\numberline {C.4}Miscellaneous tactics}{195}{section.C.4}} |
|
375 \citation{isabelle-ref} |
|
376 \citation{isabelle-ref} |
|
377 \bibstyle{abbrv} |
306 \bibdata{../manual} |
378 \bibdata{../manual} |
307 \@writefile{toc}{\contentsline {section}{\numberline {B.5}Tacticals}{148}{section.B.5}} |
379 \@writefile{toc}{\contentsline {section}{\numberline {C.5}Tacticals}{196}{section.C.5}} |
308 \bibcite{proofgeneral}{1} |
380 \bibcite{proofgeneral}{1} |
309 \bibcite{Aspinall:TACAS:2000}{2} |
381 \bibcite{Aspinall:TACAS:2000}{2} |
310 \bibcite{Bauer-Wenzel:2000:HB}{3} |
382 \bibcite{Bauer-Wenzel:2001}{3} |
311 \bibcite{Bauer-Wenzel:2001}{4} |
383 \bibcite{Berghofer-Nipkow:2000:TPHOL}{4} |
312 \bibcite{isabelle-codegen}{5} |
384 \bibcite{Bezem-Coquand:2005}{5} |
313 \bibcite{isabelle-classes}{6} |
385 \bibcite{church40}{6} |
314 \bibcite{isabelle-function}{7} |
386 \bibcite{Gentzen:1935}{7} |
315 \bibcite{OCaml}{8} |
387 \bibcite{isabelle-codegen}{8} |
316 \bibcite{SML}{9} |
388 \bibcite{isabelle-classes}{9} |
317 \bibcite{MuellerNvOS99}{10} |
389 \bibcite{isabelle-function}{10} |
318 \bibcite{NaraschewskiW-TPHOLs98}{11} |
390 \bibcite{OCaml}{11} |
319 \bibcite{isabelle-HOL}{12} |
391 \bibcite{Miller:1991}{12} |
320 \bibcite{isabelle-hol-book}{13} |
392 \bibcite{SML}{13} |
321 \bibcite{isabelle-intro}{14} |
393 \bibcite{MuellerNvOS99}{14} |
322 \bibcite{isabelle-ref}{15} |
394 \bibcite{NaraschewskiW-TPHOLs98}{15} |
323 \bibcite{isabelle-ZF}{16} |
395 \bibcite{Nipkow-TYPES02}{16} |
324 \bibcite{paulson-CADE}{17} |
396 \bibcite{isabelle-HOL}{17} |
325 \bibcite{haskell-revised-report}{18} |
397 \bibcite{isabelle-hol-book}{18} |
326 \bibcite{x-symbol}{19} |
398 \bibcite{isa-tutorial}{19} |
327 \bibcite{Wenzel:2006:Festschrift}{20} |
399 \bibcite{nipkow-prehofer}{20} |
328 \bibcite{Wenzel:1997:TPHOL}{21} |
400 \bibcite{isabelle-ref}{21} |
329 \bibcite{Wenzel:1999:TPHOL}{22} |
401 \bibcite{isabelle-ZF}{22} |
330 \bibcite{Wenzel-PhD}{23} |
402 \bibcite{paulson-natural}{23} |
331 \bibcite{isabelle-sys}{24} |
403 \bibcite{paulson-found}{24} |
332 \bibcite{Wiedijk:2000:MV}{25} |
404 \bibcite{paulson700}{25} |
|
405 \bibcite{paulson-CADE}{26} |
|
406 \bibcite{paulson-ml2}{27} |
|
407 \bibcite{haskell-revised-report}{28} |
|
408 \bibcite{Rudnicki:1992:MizarOverview}{29} |
|
409 \bibcite{Schroeder-Heister:1984}{30} |
|
410 \bibcite{Trybulec:1993:MizarFeatures}{31} |
|
411 \bibcite{isabelle-implementation}{32} |
|
412 \bibcite{Wenzel:1997:TPHOL}{33} |
|
413 \bibcite{Wenzel:1999:TPHOL}{34} |
|
414 \bibcite{Wenzel-PhD}{35} |
|
415 \bibcite{Wenzel:2006:Festschrift}{36} |
|
416 \bibcite{isabelle-sys}{37} |
|
417 \bibcite{Wenzel-Paulson:2006}{38} |
|
418 \bibcite{Wiedijk:1999:Mizar}{39} |
|
419 \bibcite{Wenzel-Wiedijk:2002}{40} |