1.1 --- a/doc-src/TutorialI/tutorial.ind Sat Jan 05 01:19:14 2002 +0100
1.2 +++ b/doc-src/TutorialI/tutorial.ind Sat Jan 05 01:20:06 2002 +0100
1.3 @@ -1,136 +1,139 @@
1.4 \begin{theindex}
1.5
1.6 - \item \ttall, \bold{201}
1.7 - \item \texttt{?}, \bold{201}
1.8 - \item \isasymuniqex, \bold{201}
1.9 - \item \ttuniquex, \bold{201}
1.10 - \item {\texttt {\&}}, \bold{201}
1.11 - \item \verb$~$, \bold{201}
1.12 - \item \verb$~=$, \bold{201}
1.13 - \item \ttor, \bold{201}
1.14 + \item \ttall, \bold{203}
1.15 + \item \texttt{?}, \bold{203}
1.16 + \item \isasymuniqex, \bold{203}
1.17 + \item \ttuniquex, \bold{203}
1.18 + \item {\texttt {\&}}, \bold{203}
1.19 + \item \verb$~$, \bold{203}
1.20 + \item \verb$~=$, \bold{203}
1.21 + \item \ttor, \bold{203}
1.22 \item \texttt{[]}, \bold{9}
1.23 \item \texttt{\#}, \bold{9}
1.24 - \item \texttt{\at}, \bold{10}, 201
1.25 - \item \isasymnotin, \bold{201}
1.26 - \item \verb$~:$, \bold{201}
1.27 - \item \isasymInter, \bold{201}
1.28 - \item \isasymUnion, \bold{201}
1.29 - \item \isasyminverse, \bold{201}
1.30 - \item \verb$^-1$, \bold{201}
1.31 - \item \isactrlsup{\isacharasterisk}, \bold{201}
1.32 - \item \verb$^$\texttt{*}, \bold{201}
1.33 - \item \isasymAnd, \bold{12}, \bold{201}
1.34 - \item \ttAnd, \bold{201}
1.35 + \item \texttt{\at}, \bold{10}, 203
1.36 + \item \isasymnotin, \bold{203}
1.37 + \item \verb$~:$, \bold{203}
1.38 + \item \isasymInter, \bold{203}
1.39 + \item \isasymUnion, \bold{203}
1.40 + \item \isasyminverse, \bold{203}
1.41 + \item \verb$^-1$, \bold{203}
1.42 + \item \isactrlsup{\isacharasterisk}, \bold{203}
1.43 + \item \verb$^$\texttt{*}, \bold{203}
1.44 + \item \isasymAnd, \bold{12}, \bold{203}
1.45 + \item \ttAnd, \bold{203}
1.46 + \item \isasymrightleftharpoons, 57
1.47 + \item \isasymrightharpoonup, 57
1.48 + \item \isasymleftharpoondown, 57
1.49 \item \emph {$\Rightarrow $}, \bold{5}
1.50 - \item \ttlbr, \bold{201}
1.51 - \item \ttrbr, \bold{201}
1.52 - \item \texttt {\%}, \bold{201}
1.53 + \item \ttlbr, \bold{203}
1.54 + \item \ttrbr, \bold{203}
1.55 + \item \texttt {\%}, \bold{203}
1.56 \item \texttt {;}, \bold{7}
1.57 \item \isa {()} (constant), 24
1.58 - \item \isa {+} (tactical), 91
1.59 + \item \isa {+} (tactical), 93
1.60 \item \isa {<*lex*>}, \see{lexicographic product}{1}
1.61 - \item \isa {?} (tactical), 91
1.62 - \item \texttt{|} (tactical), 91
1.63 + \item \isa {?} (tactical), 93
1.64 + \item \texttt{|} (tactical), 93
1.65
1.66 \indexspace
1.67
1.68 - \item \isa {0} (constant), 22, 23, 142
1.69 - \item \isa {1} (constant), 23, 142, 143
1.70 + \item \isa {0} (constant), 22, 23, 144
1.71 + \item \isa {1} (constant), 23, 144, 145
1.72
1.73 \indexspace
1.74
1.75 \item abandoning a proof, \bold{13}
1.76 \item abandoning a theory, \bold{16}
1.77 - \item \isa {abs} (constant), 145
1.78 - \item \texttt {abs}, \bold{201}
1.79 - \item absolute value, 145
1.80 + \item \isa {abs} (constant), 147
1.81 + \item \texttt {abs}, \bold{203}
1.82 + \item absolute value, 147
1.83 \item \isa {add} (modifier), 29
1.84 - \item \isa {add_ac} (theorems), 144
1.85 - \item \isa {add_assoc} (theorem), \bold{144}
1.86 - \item \isa {add_commute} (theorem), \bold{144}
1.87 - \item \isa {add_mult_distrib} (theorem), \bold{143}
1.88 - \item \texttt {ALL}, \bold{201}
1.89 - \item \isa {All} (constant), 101
1.90 - \item \isa {allE} (theorem), \bold{73}
1.91 - \item \isa {allI} (theorem), \bold{72}
1.92 + \item \isa {add_ac} (theorems), 146
1.93 + \item \isa {add_assoc} (theorem), \bold{146}
1.94 + \item \isa {add_commute} (theorem), \bold{146}
1.95 + \item \isa {add_mult_distrib} (theorem), \bold{145}
1.96 + \item \texttt {ALL}, \bold{203}
1.97 + \item \isa {All} (constant), 103
1.98 + \item \isa {allE} (theorem), \bold{75}
1.99 + \item \isa {allI} (theorem), \bold{74}
1.100 \item append function, 10--14
1.101 \item \isacommand {apply} (command), 15
1.102 - \item \isa {arg_cong} (theorem), \bold{88}
1.103 - \item \isa {arith} (method), 23, 141
1.104 + \item \isa {arg_cong} (theorem), \bold{90}
1.105 + \item \isa {arith} (method), 23, 143
1.106 \item arithmetic operations
1.107 \subitem for \protect\isa{nat}, 23
1.108 - \item \textsc {ascii} symbols, \bold{201}
1.109 - \item associative-commutative function, 168
1.110 - \item \isa {assumption} (method), 61
1.111 + \item \textsc {ascii} symbols, \bold{203}
1.112 + \item associative-commutative function, 170
1.113 + \item \isa {assumption} (method), 63
1.114 \item assumptions
1.115 \subitem of subgoal, 12
1.116 - \subitem renaming, 74--75
1.117 - \subitem reusing, 75
1.118 - \item \isa {auto} (method), 38, 84
1.119 - \item \isa {axclass}, 156--162
1.120 - \item axiom of choice, 78
1.121 - \item axiomatic type classes, 156--162
1.122 + \subitem renaming, 76--77
1.123 + \subitem reusing, 77
1.124 + \item \isa {auto} (method), 38, 86
1.125 + \item \isa {axclass}, 158--164
1.126 + \item axiom of choice, 80
1.127 + \item axiomatic type classes, 158--164
1.128
1.129 \indexspace
1.130
1.131 - \item \isacommand {back} (command), 70
1.132 - \item \isa {Ball} (constant), 101
1.133 - \item \isa {ballI} (theorem), \bold{100}
1.134 - \item \isa {best} (method), 84
1.135 - \item \isa {Bex} (constant), 101
1.136 - \item \isa {bexE} (theorem), \bold{100}
1.137 - \item \isa {bexI} (theorem), \bold{100}
1.138 - \item \isa {bij_def} (theorem), \bold{102}
1.139 - \item bijections, 102
1.140 + \item \isacommand {back} (command), 72
1.141 + \item \isa {Ball} (constant), 103
1.142 + \item \isa {ballI} (theorem), \bold{102}
1.143 + \item \isa {best} (method), 86
1.144 + \item \isa {Bex} (constant), 103
1.145 + \item \isa {bexE} (theorem), \bold{102}
1.146 + \item \isa {bexI} (theorem), \bold{102}
1.147 + \item \isa {bij_def} (theorem), \bold{104}
1.148 + \item bijections, 104
1.149 \item binary trees, 18
1.150 - \item binomial coefficients, 101
1.151 - \item bisimulations, 108
1.152 - \item \isa {blast} (method), 81--82, 84
1.153 + \item binomial coefficients, 103
1.154 + \item bisimulations, 110
1.155 + \item \isa {blast} (method), 83--84, 86
1.156 \item \isa {bool} (type), 4, 5
1.157 \item boolean expressions example, 20--22
1.158 - \item \isa {bspec} (theorem), \bold{100}
1.159 - \item \isacommand{by} (command), 65
1.160 + \item \isa {bspec} (theorem), \bold{102}
1.161 + \item \isacommand{by} (command), 67
1.162
1.163 \indexspace
1.164
1.165 - \item \isa {card} (constant), 101
1.166 - \item \isa {card_Pow} (theorem), \bold{101}
1.167 - \item \isa {card_Un_Int} (theorem), \bold{101}
1.168 - \item cardinality, 101
1.169 + \item \isa {card} (constant), 103
1.170 + \item \isa {card_Pow} (theorem), \bold{103}
1.171 + \item \isa {card_Un_Int} (theorem), \bold{103}
1.172 + \item cardinality, 103
1.173 \item \isa {case} (symbol), 32, 33
1.174 \item \isa {case} expressions, 5, 6, 18
1.175 \item case distinctions, 19
1.176 \item case splits, \bold{31}
1.177 - \item \isa {case_tac} (method), 19, 93, 149
1.178 - \item \isa {cases} (method), 154
1.179 - \item \isa {clarify} (method), 83, 84
1.180 - \item \isa {clarsimp} (method), 83, 84
1.181 - \item \isa {classical} (theorem), \bold{65}
1.182 - \item coinduction, \bold{108}
1.183 - \item \isa {Collect} (constant), 101
1.184 + \item \isa {case_tac} (method), 19, 95, 151
1.185 + \item \isa {cases} (method), 156
1.186 + \item \isa {clarify} (method), 85, 86
1.187 + \item \isa {clarsimp} (method), 85, 86
1.188 + \item \isa {classical} (theorem), \bold{67}
1.189 + \item coinduction, \bold{110}
1.190 + \item \isa {Collect} (constant), 103
1.191 \item compiling expressions example, 36--38
1.192 - \item \isa {Compl_iff} (theorem), \bold{98}
1.193 + \item \isa {Compl_iff} (theorem), \bold{100}
1.194 \item complement
1.195 - \subitem of a set, 97
1.196 + \subitem of a set, 99
1.197 \item composition
1.198 - \subitem of functions, \bold{102}
1.199 - \subitem of relations, \bold{104}
1.200 + \subitem of functions, \bold{104}
1.201 + \subitem of relations, \bold{106}
1.202 \item conclusion
1.203 \subitem of subgoal, 12
1.204 \item conditional expressions, \see{\isa{if} expressions}{1}
1.205 \item conditional simplification rules, 31
1.206 - \item \isa {cong} (attribute), 168
1.207 - \item congruence rules, \bold{167}
1.208 - \item \isa {conjE} (theorem), \bold{63}
1.209 - \item \isa {conjI} (theorem), \bold{60}
1.210 + \item \isa {cong} (attribute), 170
1.211 + \item congruence rules, \bold{169}
1.212 + \item \isa {conjE} (theorem), \bold{65}
1.213 + \item \isa {conjI} (theorem), \bold{62}
1.214 \item \isa {Cons} (constant), 9
1.215 \item \isacommand {constdefs} (command), 25
1.216 \item \isacommand {consts} (command), 10
1.217 - \item contrapositives, 65
1.218 + \item contrapositives, 67
1.219 \item converse
1.220 - \subitem of a relation, \bold{104}
1.221 - \item \isa {converse_iff} (theorem), \bold{104}
1.222 - \item CTL, 113--118, 183--185
1.223 + \subitem of a relation, \bold{106}
1.224 + \item \isa {converse_iff} (theorem), \bold{106}
1.225 + \item CTL, 115--120, 185--187
1.226
1.227 \indexspace
1.228
1.229 @@ -138,180 +141,180 @@
1.230 \item datatypes, 17--22
1.231 \subitem and nested recursion, 40, 44
1.232 \subitem mutually recursive, 38
1.233 - \subitem nested, 172
1.234 - \item \isacommand {defer} (command), 16, 92
1.235 + \subitem nested, 174
1.236 + \item \isacommand {defer} (command), 16, 94
1.237 \item Definitional Approach, 26
1.238 \item definitions, \bold{25}
1.239 \subitem unfolding, \bold{30}
1.240 \item \isacommand {defs} (command), 25
1.241 \item \isa {del} (modifier), 29
1.242 - \item description operators, 77--79
1.243 + \item description operators, 79--81
1.244 \item descriptions
1.245 - \subitem definite, 77
1.246 - \subitem indefinite, 78
1.247 - \item \isa {dest} (attribute), 94
1.248 - \item destruction rules, 63
1.249 - \item \isa {diff_mult_distrib} (theorem), \bold{143}
1.250 + \subitem definite, 79
1.251 + \subitem indefinite, 80
1.252 + \item \isa {dest} (attribute), 96
1.253 + \item destruction rules, 65
1.254 + \item \isa {diff_mult_distrib} (theorem), \bold{145}
1.255 \item difference
1.256 - \subitem of sets, \bold{98}
1.257 - \item \isa {disjCI} (theorem), \bold{66}
1.258 - \item \isa {disjE} (theorem), \bold{62}
1.259 + \subitem of sets, \bold{100}
1.260 + \item \isa {disjCI} (theorem), \bold{68}
1.261 + \item \isa {disjE} (theorem), \bold{64}
1.262 \item \isa {div} (symbol), 23
1.263 - \item divides relation, 76, 87, 93--96, 144
1.264 + \item divides relation, 78, 89, 95--98, 146
1.265 \item division
1.266 - \subitem by negative numbers, 145
1.267 - \subitem by zero, 144
1.268 - \subitem for type \protect\isa{nat}, 143
1.269 + \subitem by negative numbers, 147
1.270 + \subitem by zero, 146
1.271 + \subitem for type \protect\isa{nat}, 145
1.272 \item domain
1.273 - \subitem of a relation, 104
1.274 - \item \isa {Domain_iff} (theorem), \bold{104}
1.275 + \subitem of a relation, 106
1.276 + \item \isa {Domain_iff} (theorem), \bold{106}
1.277 \item \isacommand {done} (command), 13
1.278 - \item \isa {drule_tac} (method), 68, 88
1.279 - \item \isa {dvd_add} (theorem), \bold{144}
1.280 - \item \isa {dvd_anti_sym} (theorem), \bold{144}
1.281 - \item \isa {dvd_def} (theorem), \bold{144}
1.282 + \item \isa {drule_tac} (method), 70, 90
1.283 + \item \isa {dvd_add} (theorem), \bold{146}
1.284 + \item \isa {dvd_anti_sym} (theorem), \bold{146}
1.285 + \item \isa {dvd_def} (theorem), \bold{146}
1.286
1.287 \indexspace
1.288
1.289 - \item \isa {elim!} (attribute), 123
1.290 - \item elimination rules, 61--62
1.291 + \item \isa {elim!} (attribute), 125
1.292 + \item elimination rules, 63--64
1.293 \item \isacommand {end} (command), 14
1.294 - \item \isa {Eps} (constant), 101
1.295 + \item \isa {Eps} (constant), 103
1.296 \item equality, 5
1.297 - \subitem of functions, \bold{101}
1.298 - \subitem of records, 153
1.299 - \subitem of sets, \bold{98}
1.300 - \item \isa {equalityE} (theorem), \bold{98}
1.301 - \item \isa {equalityI} (theorem), \bold{98}
1.302 - \item \isa {erule} (method), 62
1.303 - \item \isa {erule_tac} (method), 68
1.304 - \item Euclid's algorithm, 93--96
1.305 + \subitem of functions, \bold{103}
1.306 + \subitem of records, 155
1.307 + \subitem of sets, \bold{100}
1.308 + \item \isa {equalityE} (theorem), \bold{100}
1.309 + \item \isa {equalityI} (theorem), \bold{100}
1.310 + \item \isa {erule} (method), 64
1.311 + \item \isa {erule_tac} (method), 70
1.312 + \item Euclid's algorithm, 95--98
1.313 \item even numbers
1.314 - \subitem defining inductively, 119--123
1.315 - \item \texttt {EX}, \bold{201}
1.316 - \item \isa {Ex} (constant), 101
1.317 - \item \isa {exE} (theorem), \bold{74}
1.318 - \item \isa {exI} (theorem), \bold{74}
1.319 - \item \isa {ext} (theorem), \bold{101}
1.320 - \item \isa {extend} (constant), 155
1.321 + \subitem defining inductively, 121--125
1.322 + \item \texttt {EX}, \bold{203}
1.323 + \item \isa {Ex} (constant), 103
1.324 + \item \isa {exE} (theorem), \bold{76}
1.325 + \item \isa {exI} (theorem), \bold{76}
1.326 + \item \isa {ext} (theorem), \bold{103}
1.327 + \item \isa {extend} (constant), 157
1.328 \item extensionality
1.329 - \subitem for functions, \bold{101, 102}
1.330 - \subitem for records, 153
1.331 - \subitem for sets, \bold{98}
1.332 - \item \ttEXU, \bold{201}
1.333 + \subitem for functions, \bold{103, 104}
1.334 + \subitem for records, 155
1.335 + \subitem for sets, \bold{100}
1.336 + \item \ttEXU, \bold{203}
1.337
1.338 \indexspace
1.339
1.340 \item \isa {False} (constant), 5
1.341 - \item \isa {fast} (method), 84, 116
1.342 + \item \isa {fast} (method), 86, 118
1.343 \item Fibonacci function, 47
1.344 - \item \isa {fields} (constant), 155
1.345 - \item \isa {finite} (symbol), 101
1.346 - \item \isa {Finites} (constant), 101
1.347 - \item fixed points, 108
1.348 + \item \isa {fields} (constant), 157
1.349 + \item \isa {finite} (symbol), 103
1.350 + \item \isa {Finites} (constant), 103
1.351 + \item fixed points, 110
1.352 \item flags, 5, 6, 33
1.353 \subitem setting and resetting, 5
1.354 - \item \isa {force} (method), 83, 84
1.355 + \item \isa {force} (method), 85, 86
1.356 \item formulae, 5--6
1.357 - \item forward proof, 84--90
1.358 - \item \isa {frule} (method), 75
1.359 - \item \isa {frule_tac} (method), 68
1.360 + \item forward proof, 86--92
1.361 + \item \isa {frule} (method), 77
1.362 + \item \isa {frule_tac} (method), 70
1.363 \item \isa {fst} (constant), 24
1.364 \item function types, 5
1.365 - \item functions, 101--103
1.366 - \subitem partial, 174
1.367 + \item functions, 103--105
1.368 + \subitem partial, 176
1.369 \subitem total, 11, 46--52
1.370 - \subitem underdefined, 175
1.371 + \subitem underdefined, 177
1.372
1.373 \indexspace
1.374
1.375 - \item \isa {gcd} (constant), 85--86, 93--96
1.376 - \item generalizing for induction, 121
1.377 + \item \isa {gcd} (constant), 87--88, 95--98
1.378 + \item generalizing for induction, 123
1.379 \item generalizing induction formulae, 35
1.380 - \item Girard, Jean-Yves, \fnote{63}
1.381 + \item Girard, Jean-Yves, \fnote{65}
1.382 \item Gordon, Mike, 3
1.383 \item grammars
1.384 - \subitem defining inductively, 132--137
1.385 - \item ground terms example, 127--132
1.386 + \subitem defining inductively, 134--139
1.387 + \item ground terms example, 129--134
1.388
1.389 \indexspace
1.390
1.391 \item \isa {hd} (constant), 17, 37
1.392 - \item Hilbert's $\varepsilon$-operator, 78
1.393 + \item Hilbert's $\varepsilon$-operator, 80
1.394 \item HOLCF, 43
1.395 - \item Hopcroft, J. E., 137
1.396 - \item \isa {hypreal} (type), 147
1.397 + \item Hopcroft, J. E., 139
1.398 + \item \isa {hypreal} (type), 149
1.399
1.400 \indexspace
1.401
1.402 - \item \isa {Id_def} (theorem), \bold{104}
1.403 - \item \isa {id_def} (theorem), \bold{102}
1.404 + \item \isa {Id_def} (theorem), \bold{106}
1.405 + \item \isa {id_def} (theorem), \bold{104}
1.406 \item identifiers, \bold{6}
1.407 \subitem qualified, \bold{4}
1.408 - \item identity function, \bold{102}
1.409 - \item identity relation, \bold{104}
1.410 + \item identity function, \bold{104}
1.411 + \item identity relation, \bold{106}
1.412 \item \isa {if} expressions, 5, 6
1.413 \subitem simplification of, 33
1.414 \subitem splitting of, 31, 49
1.415 \item if-and-only-if, 6
1.416 - \item \isa {iff} (attribute), 82, 94, 122
1.417 - \item \isa {iffD1} (theorem), \bold{86}
1.418 - \item \isa {iffD2} (theorem), \bold{86}
1.419 + \item \isa {iff} (attribute), 84, 96, 124
1.420 + \item \isa {iffD1} (theorem), \bold{88}
1.421 + \item \isa {iffD2} (theorem), \bold{88}
1.422 \item image
1.423 - \subitem under a function, \bold{103}
1.424 - \subitem under a relation, \bold{104}
1.425 - \item \isa {image_def} (theorem), \bold{103}
1.426 - \item \isa {Image_iff} (theorem), \bold{104}
1.427 - \item \isa {impI} (theorem), \bold{64}
1.428 - \item implication, 64--65
1.429 - \item \isa {ind_cases} (method), 123
1.430 - \item \isa {induct_tac} (method), 12, 19, 52, 182
1.431 - \item induction, 178--185
1.432 - \subitem complete, 180
1.433 - \subitem deriving new schemas, 182
1.434 - \subitem on a term, 179
1.435 + \subitem under a function, \bold{105}
1.436 + \subitem under a relation, \bold{106}
1.437 + \item \isa {image_def} (theorem), \bold{105}
1.438 + \item \isa {Image_iff} (theorem), \bold{106}
1.439 + \item \isa {impI} (theorem), \bold{66}
1.440 + \item implication, 66--67
1.441 + \item \isa {ind_cases} (method), 125
1.442 + \item \isa {induct_tac} (method), 12, 19, 52, 184
1.443 + \item induction, 180--187
1.444 + \subitem complete, 182
1.445 + \subitem deriving new schemas, 184
1.446 + \subitem on a term, 181
1.447 \subitem recursion, 51--52
1.448 \subitem structural, 19
1.449 - \subitem well-founded, 107
1.450 + \subitem well-founded, 109
1.451 \item induction heuristics, 34--36
1.452 - \item \isacommand {inductive} (command), 119
1.453 + \item \isacommand {inductive} (command), 121
1.454 \item inductive definition
1.455 - \subitem simultaneous, 133
1.456 - \item inductive definitions, 119--137
1.457 - \item \isacommand {inductive\_cases} (command), 123, 131
1.458 + \subitem simultaneous, 135
1.459 + \item inductive definitions, 121--139
1.460 + \item \isacommand {inductive\_cases} (command), 125, 133
1.461 \item infinitely branching trees, 43
1.462 \item infix annotations, \bold{54}
1.463 \item \isacommand{infixr} (annotation), 10
1.464 - \item \isa {inj_on_def} (theorem), \bold{102}
1.465 - \item injections, 102
1.466 - \item \isa {insert} (constant), 99
1.467 - \item \isa {insert} (method), 89--90
1.468 - \item instance, \bold{158}
1.469 - \item \texttt {INT}, \bold{201}
1.470 - \item \texttt {Int}, \bold{201}
1.471 - \item \isa {int} (type), 145--146
1.472 - \item \isa {INT_iff} (theorem), \bold{100}
1.473 - \item \isa {IntD1} (theorem), \bold{97}
1.474 - \item \isa {IntD2} (theorem), \bold{97}
1.475 - \item integers, 145--146
1.476 - \item \isa {INTER} (constant), 101
1.477 - \item \texttt {Inter}, \bold{201}
1.478 - \item \isa {Inter_iff} (theorem), \bold{100}
1.479 - \item intersection, 97
1.480 - \subitem indexed, 100
1.481 - \item \isa {IntI} (theorem), \bold{97}
1.482 - \item \isa {intro} (method), 66
1.483 - \item \isa {intro!} (attribute), 120
1.484 - \item \isa {intro_classes} (method), 158
1.485 - \item introduction rules, 60--61
1.486 - \item \isa {inv} (constant), 78
1.487 - \item \isa {inv_image_def} (theorem), \bold{107}
1.488 + \item \isa {inj_on_def} (theorem), \bold{104}
1.489 + \item injections, 104
1.490 + \item \isa {insert} (constant), 101
1.491 + \item \isa {insert} (method), 91--92
1.492 + \item instance, \bold{160}
1.493 + \item \texttt {INT}, \bold{203}
1.494 + \item \texttt {Int}, \bold{203}
1.495 + \item \isa {int} (type), 147--148
1.496 + \item \isa {INT_iff} (theorem), \bold{102}
1.497 + \item \isa {IntD1} (theorem), \bold{99}
1.498 + \item \isa {IntD2} (theorem), \bold{99}
1.499 + \item integers, 147--148
1.500 + \item \isa {INTER} (constant), 103
1.501 + \item \texttt {Inter}, \bold{203}
1.502 + \item \isa {Inter_iff} (theorem), \bold{102}
1.503 + \item intersection, 99
1.504 + \subitem indexed, 102
1.505 + \item \isa {IntI} (theorem), \bold{99}
1.506 + \item \isa {intro} (method), 68
1.507 + \item \isa {intro!} (attribute), 122
1.508 + \item \isa {intro_classes} (method), 160
1.509 + \item introduction rules, 62--63
1.510 + \item \isa {inv} (constant), 80
1.511 + \item \isa {inv_image_def} (theorem), \bold{109}
1.512 \item inverse
1.513 - \subitem of a function, \bold{102}
1.514 - \subitem of a relation, \bold{104}
1.515 + \subitem of a function, \bold{104}
1.516 + \subitem of a relation, \bold{106}
1.517 \item inverse image
1.518 - \subitem of a function, 103
1.519 - \subitem of a relation, 106
1.520 + \subitem of a function, 105
1.521 + \subitem of a relation, 108
1.522 \item \isa {itrev} (constant), 34
1.523
1.524 \indexspace
1.525 @@ -322,180 +325,182 @@
1.526
1.527 \item $\lambda$ expressions, 5
1.528 \item LCF, 43
1.529 - \item \isa {LEAST} (symbol), 23, 77
1.530 - \item least number operator, \see{\protect\isa{LEAST}}{77}
1.531 + \item \isa {LEAST} (symbol), 23, 79
1.532 + \item least number operator, \see{\protect\isa{LEAST}}{79}
1.533 \item Leibniz, Gottfried Wilhelm, 53
1.534 \item \isacommand {lemma} (command), 13
1.535 - \item \isacommand {lemmas} (command), 85, 94
1.536 + \item \isacommand {lemmas} (command), 87, 96
1.537 \item \isa {length} (symbol), 18
1.538 - \item \isa {length_induct}, \bold{182}
1.539 - \item \isa {less_than} (constant), 106
1.540 - \item \isa {less_than_iff} (theorem), \bold{106}
1.541 + \item \isa {length_induct}, \bold{184}
1.542 + \item \isa {less_than} (constant), 108
1.543 + \item \isa {less_than_iff} (theorem), \bold{108}
1.544 \item \isa {let} expressions, 5, 6, 31
1.545 \item \isa {Let_def} (theorem), 31
1.546 - \item \isa {lex_prod_def} (theorem), \bold{107}
1.547 - \item lexicographic product, \bold{107}, 170
1.548 + \item \isa {lex_prod_def} (theorem), \bold{109}
1.549 + \item lexicographic product, \bold{109}, 172
1.550 \item {\texttt{lfp}}
1.551 - \subitem applications of, \see{CTL}{108}
1.552 + \subitem applications of, \see{CTL}{110}
1.553 \item Library, 4
1.554 - \item linear arithmetic, 22--24, 141
1.555 + \item linear arithmetic, 22--24, 143
1.556 \item \isa {List} (theory), 17
1.557 \item \isa {list} (type), 5, 9, 17
1.558 \item \isa {list.split} (theorem), 32
1.559 - \item \isa {lists_mono} (theorem), \bold{129}
1.560 - \item Lowe, Gavin, 188--189
1.561 + \item \isa {lists_mono} (theorem), \bold{131}
1.562 + \item Lowe, Gavin, 190--191
1.563
1.564 \indexspace
1.565
1.566 \item \isa {Main} (theory), 4
1.567 - \item major premise, \bold{67}
1.568 - \item \isa {make} (constant), 155
1.569 + \item major premise, \bold{69}
1.570 + \item \isa {make} (constant), 157
1.571 \item \isa {max} (constant), 23, 24
1.572 - \item measure functions, 47, 106
1.573 - \item \isa {measure_def} (theorem), \bold{107}
1.574 - \item meta-logic, \bold{72}
1.575 + \item measure functions, 47, 108
1.576 + \item \isa {measure_def} (theorem), \bold{109}
1.577 + \item meta-logic, \bold{74}
1.578 \item methods, \bold{16}
1.579 \item \isa {min} (constant), 23, 24
1.580 \item mixfix annotations, \bold{53}
1.581 \item \isa {mod} (symbol), 23
1.582 - \item \isa {mod_div_equality} (theorem), \bold{143}
1.583 - \item \isa {mod_mult_distrib} (theorem), \bold{143}
1.584 - \item model checking example, 108--118
1.585 - \item \emph{modus ponens}, 59, 64
1.586 - \item \isa {mono_def} (theorem), \bold{108}
1.587 - \item monotone functions, \bold{108}, 131
1.588 - \subitem and inductive definitions, 129--130
1.589 - \item \isa {more} (constant), 150, 152
1.590 - \item \isa {mp} (theorem), \bold{64}
1.591 - \item \isa {mult_ac} (theorems), 144
1.592 - \item multiple inheritance, \bold{161}
1.593 - \item multiset ordering, \bold{107}
1.594 + \item \isa {mod_div_equality} (theorem), \bold{145}
1.595 + \item \isa {mod_mult_distrib} (theorem), \bold{145}
1.596 + \item model checking example, 110--120
1.597 + \item \emph{modus ponens}, 61, 66
1.598 + \item \isa {mono_def} (theorem), \bold{110}
1.599 + \item monotone functions, \bold{110}, 133
1.600 + \subitem and inductive definitions, 131--132
1.601 + \item \isa {more} (constant), 152, 154
1.602 + \item \isa {mp} (theorem), \bold{66}
1.603 + \item \isa {mult_ac} (theorems), 146
1.604 + \item multiple inheritance, \bold{163}
1.605 + \item multiset ordering, \bold{109}
1.606
1.607 \indexspace
1.608
1.609 - \item \isa {nat} (type), 4, 22, 143--145
1.610 - \item \isa {nat_less_induct} (theorem), 180
1.611 - \item natural deduction, 59--60
1.612 - \item natural numbers, 22, 143--145
1.613 - \item Needham-Schroeder protocol, 187--189
1.614 - \item negation, 65--67
1.615 + \item \isa {nat} (type), 4, 22, 145--147
1.616 + \item \isa {nat_less_induct} (theorem), 182
1.617 + \item natural deduction, 61--62
1.618 + \item natural numbers, 22, 145--147
1.619 + \item Needham-Schroeder protocol, 189--191
1.620 + \item negation, 67--69
1.621 \item \isa {Nil} (constant), 9
1.622 \item \isa {no_asm} (modifier), 29
1.623 \item \isa {no_asm_simp} (modifier), 30
1.624 \item \isa {no_asm_use} (modifier), 30
1.625 - \item non-standard reals, 147
1.626 + \item non-standard reals, 149
1.627 \item \isa {None} (constant), \bold{24}
1.628 - \item \isa {notE} (theorem), \bold{65}
1.629 - \item \isa {notI} (theorem), \bold{65}
1.630 - \item numbers, 141--147
1.631 - \item numeric literals, 142
1.632 - \subitem for type \protect\isa{nat}, 143
1.633 - \subitem for type \protect\isa{real}, 147
1.634 + \item \isa {notE} (theorem), \bold{67}
1.635 + \item \isa {notI} (theorem), \bold{67}
1.636 + \item numbers, 143--149
1.637 + \item numeric literals, 144
1.638 + \subitem for type \protect\isa{nat}, 145
1.639 + \subitem for type \protect\isa{real}, 149
1.640
1.641 \indexspace
1.642
1.643 - \item \isa {O} (symbol), 104
1.644 - \item \texttt {o}, \bold{201}
1.645 - \item \isa {o_def} (theorem), \bold{102}
1.646 - \item \isa {OF} (attribute), 87--88
1.647 - \item \isa {of} (attribute), 85, 88
1.648 + \item \isa {O} (symbol), 106
1.649 + \item \texttt {o}, \bold{203}
1.650 + \item \isa {o_def} (theorem), \bold{104}
1.651 + \item \isa {OF} (attribute), 89--90
1.652 + \item \isa {of} (attribute), 87, 90
1.653 \item \isa {only} (modifier), 29
1.654 \item \isacommand {oops} (command), 13
1.655 \item \isa {option} (type), \bold{24}
1.656 - \item ordered rewriting, \bold{168}
1.657 - \item overloading, 23, 157--159
1.658 - \subitem and arithmetic, 142
1.659 + \item ordered rewriting, \bold{170}
1.660 + \item overloading, 23, 159--161
1.661 + \subitem and arithmetic, 144
1.662
1.663 \indexspace
1.664
1.665 - \item pairs and tuples, 24, 147--150
1.666 + \item pairs and tuples, 24, 149--152
1.667 \item parent theories, \bold{4}
1.668 \item pattern matching
1.669 \subitem and \isacommand{recdef}, 47
1.670 \item patterns
1.671 - \subitem higher-order, \bold{169}
1.672 - \item PDL, 110--112
1.673 - \item \isacommand {pr} (command), 16, 92
1.674 - \item \isacommand {prefer} (command), 16, 92
1.675 + \subitem higher-order, \bold{171}
1.676 + \item PDL, 112--114
1.677 + \item \isacommand {pr} (command), 16, 94
1.678 + \item \isacommand {prefer} (command), 16, 94
1.679 + \item prefix annotation, \bold{56}
1.680 \item primitive recursion, \see{recursion, primitive}{1}
1.681 \item \isacommand {primrec} (command), 10, 18, 38--43
1.682 + \item print mode, 55
1.683 \item \isacommand {print\_syntax} (command), 54
1.684 \item product type, \see{pairs and tuples}{1}
1.685 \item Proof General, \bold{7}
1.686 \item proof state, 12
1.687 \item proofs
1.688 \subitem abandoning, \bold{13}
1.689 - \subitem examples of failing, 79--81
1.690 + \subitem examples of failing, 81--83
1.691 \item protocols
1.692 - \subitem security, 187--197
1.693 + \subitem security, 189--199
1.694
1.695 \indexspace
1.696
1.697 \item quantifiers, 6
1.698 - \subitem and inductive definitions, 127--129
1.699 - \subitem existential, 74
1.700 - \subitem for sets, 100
1.701 - \subitem instantiating, 76
1.702 - \subitem universal, 71--74
1.703 + \subitem and inductive definitions, 129--131
1.704 + \subitem existential, 76
1.705 + \subitem for sets, 102
1.706 + \subitem instantiating, 78
1.707 + \subitem universal, 73--76
1.708
1.709 \indexspace
1.710
1.711 - \item \isa {r_into_rtrancl} (theorem), \bold{104}
1.712 - \item \isa {r_into_trancl} (theorem), \bold{105}
1.713 + \item \isa {r_into_rtrancl} (theorem), \bold{106}
1.714 + \item \isa {r_into_trancl} (theorem), \bold{107}
1.715 \item range
1.716 - \subitem of a function, 103
1.717 - \subitem of a relation, 104
1.718 - \item \isa {range} (symbol), 103
1.719 - \item \isa {Range_iff} (theorem), \bold{104}
1.720 - \item \isa {Real} (theory), 147
1.721 - \item \isa {real} (type), 146--147
1.722 - \item real numbers, 146--147
1.723 - \item \isacommand {recdef} (command), 46--52, 106, 170--178
1.724 - \subitem and numeric literals, 142
1.725 - \item \isa {recdef_cong} (attribute), 174
1.726 + \subitem of a function, 105
1.727 + \subitem of a relation, 106
1.728 + \item \isa {range} (symbol), 105
1.729 + \item \isa {Range_iff} (theorem), \bold{106}
1.730 + \item \isa {Real} (theory), 149
1.731 + \item \isa {real} (type), 148--149
1.732 + \item real numbers, 148--149
1.733 + \item \isacommand {recdef} (command), 46--52, 108, 172--180
1.734 + \subitem and numeric literals, 144
1.735 + \item \isa {recdef_cong} (attribute), 176
1.736 \item \isa {recdef_simp} (attribute), 49
1.737 - \item \isa {recdef_wf} (attribute), 172
1.738 - \item \isacommand {record} (command), 151
1.739 - \item records, 150--156
1.740 - \subitem extensible, 152
1.741 + \item \isa {recdef_wf} (attribute), 174
1.742 + \item \isacommand {record} (command), 153
1.743 + \item records, 152--158
1.744 + \subitem extensible, 154--155
1.745 \item recursion
1.746 - \subitem guarded, 175
1.747 + \subitem guarded, 177
1.748 \subitem primitive, 18
1.749 - \subitem well-founded, \bold{171}
1.750 + \subitem well-founded, \bold{173}
1.751 \item recursion induction, 51--52
1.752 \item \isacommand {redo} (command), 16
1.753 - \item reflexive and transitive closure, 104--106
1.754 + \item reflexive and transitive closure, 106--108
1.755 \item reflexive transitive closure
1.756 - \subitem defining inductively, 124--127
1.757 - \item \isa {rel_comp_def} (theorem), \bold{104}
1.758 - \item relations, 103--106
1.759 - \subitem well-founded, 106--107
1.760 - \item \isa {rename_tac} (method), 74--75
1.761 + \subitem defining inductively, 126--129
1.762 + \item \isa {rel_comp_def} (theorem), \bold{106}
1.763 + \item relations, 105--108
1.764 + \subitem well-founded, 108--109
1.765 + \item \isa {rename_tac} (method), 76--77
1.766 \item \isa {rev} (constant), 10--14, 34
1.767 \item rewrite rules, \bold{27}
1.768 - \subitem permutative, \bold{168}
1.769 + \subitem permutative, \bold{170}
1.770 \item rewriting, \bold{27}
1.771 \item \isa {rotate_tac} (method), 30
1.772 - \item \isa {rtrancl_refl} (theorem), \bold{104}
1.773 - \item \isa {rtrancl_trans} (theorem), \bold{104}
1.774 - \item rule induction, 120--122
1.775 - \item rule inversion, 122--123, 131--132
1.776 - \item \isa {rule_format} (attribute), 179
1.777 - \item \isa {rule_tac} (method), 68
1.778 - \subitem and renaming, 75
1.779 + \item \isa {rtrancl_refl} (theorem), \bold{106}
1.780 + \item \isa {rtrancl_trans} (theorem), \bold{106}
1.781 + \item rule induction, 122--124
1.782 + \item rule inversion, 124--125, 133--134
1.783 + \item \isa {rule_format} (attribute), 181
1.784 + \item \isa {rule_tac} (method), 70
1.785 + \subitem and renaming, 77
1.786
1.787 \indexspace
1.788
1.789 - \item \isa {safe} (method), 83, 84
1.790 - \item safe rules, \bold{82}
1.791 + \item \isa {safe} (method), 85, 86
1.792 + \item safe rules, \bold{84}
1.793 \item selector
1.794 - \subitem record, 151
1.795 - \item \isa {set} (type), 5, 97
1.796 - \item set comprehensions, 99--100
1.797 - \item \isa {set_ext} (theorem), \bold{98}
1.798 - \item sets, 97--101
1.799 - \subitem finite, 101
1.800 - \subitem notation for finite, \bold{99}
1.801 + \subitem record, 153
1.802 + \item \isa {set} (type), 5, 99
1.803 + \item set comprehensions, 101--102
1.804 + \item \isa {set_ext} (theorem), \bold{100}
1.805 + \item sets, 99--103
1.806 + \subitem finite, 103
1.807 + \subitem notation for finite, \bold{101}
1.808 \item settings, \see{flags}{1}
1.809 \item \isa {show_brackets} (flag), 6
1.810 \item \isa {show_types} (flag), 5, 16
1.811 @@ -503,60 +508,63 @@
1.812 \item \isa {simp} (method), \bold{28}
1.813 \item \isa {simp} del (attribute), 28
1.814 \item \isa {simp_all} (method), 29, 38
1.815 - \item simplification, 27--33, 167--170
1.816 + \item simplification, 27--33, 169--172
1.817 \subitem of \isa{let}-expressions, 31
1.818 \subitem with definitions, 30
1.819 \subitem with/of assumptions, 29
1.820 - \item simplification rule, 169--170
1.821 + \item simplification rule, 171--172
1.822 \item simplification rules, 28
1.823 \subitem adding and deleting, 29
1.824 - \item \isa {simplified} (attribute), 85, 88
1.825 + \item \isa {simplified} (attribute), 87, 90
1.826 \item \isa {size} (constant), 17
1.827 \item \isa {snd} (constant), 24
1.828 - \item \isa {SOME} (symbol), 78
1.829 - \item \texttt {SOME}, \bold{201}
1.830 + \item \isa {SOME} (symbol), 80
1.831 + \item \texttt {SOME}, \bold{203}
1.832 \item \isa {Some} (constant), \bold{24}
1.833 - \item \isa {some_equality} (theorem), \bold{78}
1.834 - \item \isa {someI} (theorem), \bold{78}
1.835 - \item \isa {someI2} (theorem), \bold{78}
1.836 - \item \isa {someI_ex} (theorem), \bold{79}
1.837 - \item sorts, 162
1.838 - \item \isa {spec} (theorem), \bold{72}
1.839 + \item \isa {some_equality} (theorem), \bold{80}
1.840 + \item \isa {someI} (theorem), \bold{80}
1.841 + \item \isa {someI2} (theorem), \bold{80}
1.842 + \item \isa {someI_ex} (theorem), \bold{81}
1.843 + \item sorts, 164
1.844 + \item \isa {spec} (theorem), \bold{74}
1.845 \item \isa {split} (attribute), 32
1.846 - \item \isa {split} (constant), 148
1.847 - \item \isa {split} (method), 31, 148
1.848 + \item \isa {split} (constant), 150
1.849 + \item \isa {split} (method), 31, 150
1.850 \item \isa {split} (modifier), 32
1.851 \item split rule, \bold{32}
1.852 \item \isa {split_if} (theorem), 32
1.853 \item \isa {split_if_asm} (theorem), 32
1.854 - \item \isa {ssubst} (theorem), \bold{69}
1.855 + \item \isa {ssubst} (theorem), \bold{71}
1.856 \item structural induction, \see{induction, structural}{1}
1.857 - \item subclasses, 156, 161
1.858 + \item subclasses, 158, 163
1.859 \item subgoal numbering, 46
1.860 - \item \isa {subgoal_tac} (method), 90
1.861 + \item \isa {subgoal_tac} (method), 92
1.862 \item subgoals, 12
1.863 - \item subset relation, \bold{98}
1.864 - \item \isa {subsetD} (theorem), \bold{98}
1.865 - \item \isa {subsetI} (theorem), \bold{98}
1.866 - \item \isa {subst} (method), 69
1.867 - \item substitution, 69--71
1.868 + \item subset relation, \bold{100}
1.869 + \item \isa {subsetD} (theorem), \bold{100}
1.870 + \item \isa {subsetI} (theorem), \bold{100}
1.871 + \item \isa {subst} (method), 71
1.872 + \item substitution, 71--73
1.873 \item \isa {Suc} (constant), 22
1.874 - \item \isa {surj_def} (theorem), \bold{102}
1.875 - \item surjections, 102
1.876 - \item \isa {sym} (theorem), \bold{86}
1.877 + \item \isa {surj_def} (theorem), \bold{104}
1.878 + \item surjections, 104
1.879 + \item \isa {sym} (theorem), \bold{88}
1.880 + \item symbols, \bold{55}
1.881 \item syntax, 6, 11
1.882 + \item \isacommand {syntax} (command), 56
1.883 + \item syntax translations, 57
1.884
1.885 \indexspace
1.886
1.887 - \item tacticals, 91
1.888 + \item tacticals, 93
1.889 \item tactics, 12
1.890 \item \isacommand {term} (command), 16
1.891 \item term rewriting, \bold{27}
1.892 \item termination, \see{functions, total}{1}
1.893 \item terms, 5
1.894 - \item \isa {THE} (symbol), 77
1.895 - \item \isa {the_equality} (theorem), \bold{77}
1.896 - \item \isa {THEN} (attribute), \bold{86}, 88, 94
1.897 + \item \isa {THE} (symbol), 79
1.898 + \item \isa {the_equality} (theorem), \bold{79}
1.899 + \item \isa {THEN} (attribute), \bold{88}, 90, 96
1.900 \item \isacommand {theorem} (command), \bold{11}, 13
1.901 \item theories, 4
1.902 \subitem abandoning, \bold{16}
1.903 @@ -567,11 +575,12 @@
1.904 \item \isa {ToyList} example, 9--14
1.905 \item \isa {trace_simp} (flag), 33
1.906 \item tracing the simplifier, \bold{33}
1.907 - \item \isa {trancl_trans} (theorem), \bold{105}
1.908 - \item transition systems, 109
1.909 + \item \isa {trancl_trans} (theorem), \bold{107}
1.910 + \item transition systems, 111
1.911 + \item \isacommand {translations} (command), 57
1.912 \item tries, 44--46
1.913 \item \isa {True} (constant), 5
1.914 - \item \isa {truncate} (constant), 155
1.915 + \item \isa {truncate} (constant), 157
1.916 \item tuples, \see{pairs and tuples}{1}
1.917 \item \isacommand {typ} (command), 16
1.918 \item type constraints, \bold{6}
1.919 @@ -579,60 +588,61 @@
1.920 \item type inference, \bold{5}
1.921 \item type synonyms, 25
1.922 \item type variables, 5
1.923 - \item \isacommand {typedecl} (command), 109, 163
1.924 - \item \isacommand {typedef} (command), 163--166
1.925 + \item \isacommand {typedecl} (command), 111, 165
1.926 + \item \isacommand {typedef} (command), 165--168
1.927 \item types, 4--5
1.928 - \subitem declaring, 163
1.929 - \subitem defining, 163--166
1.930 + \subitem declaring, 165
1.931 + \subitem defining, 165--168
1.932 \item \isacommand {types} (command), 25
1.933
1.934 \indexspace
1.935
1.936 - \item Ullman, J. D., 137
1.937 - \item \texttt {UN}, \bold{201}
1.938 - \item \texttt {Un}, \bold{201}
1.939 - \item \isa {UN_E} (theorem), \bold{100}
1.940 - \item \isa {UN_I} (theorem), \bold{100}
1.941 - \item \isa {UN_iff} (theorem), \bold{100}
1.942 - \item \isa {Un_subset_iff} (theorem), \bold{98}
1.943 + \item Ullman, J. D., 139
1.944 + \item \texttt {UN}, \bold{203}
1.945 + \item \texttt {Un}, \bold{203}
1.946 + \item \isa {UN_E} (theorem), \bold{102}
1.947 + \item \isa {UN_I} (theorem), \bold{102}
1.948 + \item \isa {UN_iff} (theorem), \bold{102}
1.949 + \item \isa {Un_subset_iff} (theorem), \bold{100}
1.950 \item \isacommand {undo} (command), 16
1.951 \item \isa {unfold} (method), \bold{31}
1.952 - \item unification, 68--71
1.953 - \item \isa {UNION} (constant), 101
1.954 - \item \texttt {Union}, \bold{201}
1.955 + \item Unicode, 55
1.956 + \item unification, 70--73
1.957 + \item \isa {UNION} (constant), 103
1.958 + \item \texttt {Union}, \bold{203}
1.959 \item union
1.960 - \subitem indexed, 100
1.961 - \item \isa {Union_iff} (theorem), \bold{100}
1.962 + \subitem indexed, 102
1.963 + \item \isa {Union_iff} (theorem), \bold{102}
1.964 \item \isa {unit} (type), 24
1.965 - \item unknowns, 7, \bold{60}
1.966 - \item unsafe rules, \bold{82}
1.967 + \item unknowns, 7, \bold{62}
1.968 + \item unsafe rules, \bold{84}
1.969 \item update
1.970 - \subitem record, 151
1.971 - \item updating a function, \bold{101}
1.972 + \subitem record, 153
1.973 + \item updating a function, \bold{103}
1.974
1.975 \indexspace
1.976
1.977 \item variables, 7
1.978 \subitem schematic, 7
1.979 \subitem type, 5
1.980 - \item \isa {vimage_def} (theorem), \bold{103}
1.981 + \item \isa {vimage_def} (theorem), \bold{105}
1.982
1.983 \indexspace
1.984
1.985 \item Wenzel, Markus, vii
1.986 - \item \isa {wf_induct} (theorem), \bold{107}
1.987 - \item \isa {wf_inv_image} (theorem), \bold{107}
1.988 - \item \isa {wf_less_than} (theorem), \bold{106}
1.989 - \item \isa {wf_lex_prod} (theorem), \bold{107}
1.990 - \item \isa {wf_measure} (theorem), \bold{107}
1.991 - \item \isa {wf_subset} (theorem), 172
1.992 - \item \isa {while} (constant), 177
1.993 - \item \isa {While_Combinator} (theory), 177
1.994 - \item \isa {while_rule} (theorem), 177
1.995 + \item \isa {wf_induct} (theorem), \bold{109}
1.996 + \item \isa {wf_inv_image} (theorem), \bold{109}
1.997 + \item \isa {wf_less_than} (theorem), \bold{108}
1.998 + \item \isa {wf_lex_prod} (theorem), \bold{109}
1.999 + \item \isa {wf_measure} (theorem), \bold{109}
1.1000 + \item \isa {wf_subset} (theorem), 174
1.1001 + \item \isa {while} (constant), 179
1.1002 + \item \isa {While_Combinator} (theory), 179
1.1003 + \item \isa {while_rule} (theorem), 179
1.1004
1.1005 \indexspace
1.1006
1.1007 - \item \isa {zadd_ac} (theorems), 145
1.1008 - \item \isa {zmult_ac} (theorems), 145
1.1009 + \item \isa {zadd_ac} (theorems), 147
1.1010 + \item \isa {zmult_ac} (theorems), 147
1.1011
1.1012 \end{theindex}