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