1.1 --- a/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:20:52 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:27:32 2002 +0100
1.3 @@ -246,7 +246,7 @@
1.4 Here the degenerate mixfix annotations on the rightmost column
1.5 happen to consist of a single Isabelle symbol each:
1.6 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
1.7 - \verb,\,\verb,<yen>,, and \verb,\,$,.
1.8 + \verb,\,\verb,<yen>,, and \verb,$,.
1.9
1.10 Recall that a constructor like @{text Euro} actually is a function
1.11 @{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will
2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:20:52 2002 +0100
2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:27:32 2002 +0100
2.3 @@ -244,7 +244,7 @@
2.4 Here the degenerate mixfix annotations on the rightmost column
2.5 happen to consist of a single Isabelle symbol each:
2.6 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
2.7 - \verb,\,\verb,<yen>,, and \verb,\,\verb,<dollar>,.
2.8 + \verb,\,\verb,<yen>,, and \verb,$,.
2.9
2.10 Recall that a constructor like \isa{Euro} actually is a function
2.11 \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
3.1 --- a/doc-src/TutorialI/tutorial.ind Sat Jan 05 01:20:52 2002 +0100
3.2 +++ b/doc-src/TutorialI/tutorial.ind Sat Jan 05 01:27:32 2002 +0100
3.3 @@ -10,7 +10,7 @@
3.4 \item \ttor, \bold{203}
3.5 \item \texttt{[]}, \bold{9}
3.6 \item \texttt{\#}, \bold{9}
3.7 - \item \texttt{\at}, \bold{10}, 203
3.8 + \item \texttt{\at}, \bold{10}, \hyperpage{203}
3.9 \item \isasymnotin, \bold{203}
3.10 \item \verb$~:$, \bold{203}
3.11 \item \isasymInter, \bold{203}
3.12 @@ -21,229 +21,233 @@
3.13 \item \verb$^$\texttt{*}, \bold{203}
3.14 \item \isasymAnd, \bold{12}, \bold{203}
3.15 \item \ttAnd, \bold{203}
3.16 - \item \isasymrightleftharpoons, 57
3.17 - \item \isasymrightharpoonup, 57
3.18 - \item \isasymleftharpoondown, 57
3.19 + \item \isasymrightleftharpoons, \hyperpage{57}
3.20 + \item \isasymrightharpoonup, \hyperpage{57}
3.21 + \item \isasymleftharpoondown, \hyperpage{57}
3.22 \item \emph {$\Rightarrow $}, \bold{5}
3.23 \item \ttlbr, \bold{203}
3.24 \item \ttrbr, \bold{203}
3.25 \item \texttt {\%}, \bold{203}
3.26 \item \texttt {;}, \bold{7}
3.27 - \item \isa {()} (constant), 24
3.28 - \item \isa {+} (tactical), 93
3.29 + \item \isa {()} (constant), \hyperpage{24}
3.30 + \item \isa {+} (tactical), \hyperpage{93}
3.31 \item \isa {<*lex*>}, \see{lexicographic product}{1}
3.32 - \item \isa {?} (tactical), 93
3.33 - \item \texttt{|} (tactical), 93
3.34 + \item \isa {?} (tactical), \hyperpage{93}
3.35 + \item \texttt{|} (tactical), \hyperpage{93}
3.36
3.37 \indexspace
3.38
3.39 - \item \isa {0} (constant), 22, 23, 144
3.40 - \item \isa {1} (constant), 23, 144, 145
3.41 + \item \isa {0} (constant), \hyperpage{22, 23}, \hyperpage{144}
3.42 + \item \isa {1} (constant), \hyperpage{23}, \hyperpage{144, 145}
3.43
3.44 \indexspace
3.45
3.46 \item abandoning a proof, \bold{13}
3.47 \item abandoning a theory, \bold{16}
3.48 - \item \isa {abs} (constant), 147
3.49 + \item \isa {abs} (constant), \hyperpage{147}
3.50 \item \texttt {abs}, \bold{203}
3.51 - \item absolute value, 147
3.52 - \item \isa {add} (modifier), 29
3.53 - \item \isa {add_ac} (theorems), 146
3.54 + \item absolute value, \hyperpage{147}
3.55 + \item \isa {add} (modifier), \hyperpage{29}
3.56 + \item \isa {add_ac} (theorems), \hyperpage{146}
3.57 \item \isa {add_assoc} (theorem), \bold{146}
3.58 \item \isa {add_commute} (theorem), \bold{146}
3.59 \item \isa {add_mult_distrib} (theorem), \bold{145}
3.60 \item \texttt {ALL}, \bold{203}
3.61 - \item \isa {All} (constant), 103
3.62 + \item \isa {All} (constant), \hyperpage{103}
3.63 \item \isa {allE} (theorem), \bold{75}
3.64 \item \isa {allI} (theorem), \bold{74}
3.65 - \item append function, 10--14
3.66 - \item \isacommand {apply} (command), 15
3.67 + \item append function, \hyperpage{10--14}
3.68 + \item \isacommand {apply} (command), \hyperpage{15}
3.69 \item \isa {arg_cong} (theorem), \bold{90}
3.70 - \item \isa {arith} (method), 23, 143
3.71 + \item \isa {arith} (method), \hyperpage{23}, \hyperpage{143}
3.72 \item arithmetic operations
3.73 - \subitem for \protect\isa{nat}, 23
3.74 + \subitem for \protect\isa{nat}, \hyperpage{23}
3.75 \item \textsc {ascii} symbols, \bold{203}
3.76 - \item associative-commutative function, 170
3.77 - \item \isa {assumption} (method), 63
3.78 + \item Aspinall, David, \hyperpage{viii}
3.79 + \item associative-commutative function, \hyperpage{170}
3.80 + \item \isa {assumption} (method), \hyperpage{63}
3.81 \item assumptions
3.82 - \subitem of subgoal, 12
3.83 - \subitem renaming, 76--77
3.84 - \subitem reusing, 77
3.85 - \item \isa {auto} (method), 38, 86
3.86 - \item \isa {axclass}, 158--164
3.87 - \item axiom of choice, 80
3.88 - \item axiomatic type classes, 158--164
3.89 + \subitem of subgoal, \hyperpage{12}
3.90 + \subitem renaming, \hyperpage{76--77}
3.91 + \subitem reusing, \hyperpage{77}
3.92 + \item \isa {auto} (method), \hyperpage{38}, \hyperpage{86}
3.93 + \item \isa {axclass}, \hyperpage{158--164}
3.94 + \item axiom of choice, \hyperpage{80}
3.95 + \item axiomatic type classes, \hyperpage{158--164}
3.96
3.97 \indexspace
3.98
3.99 - \item \isacommand {back} (command), 72
3.100 - \item \isa {Ball} (constant), 103
3.101 + \item \isacommand {back} (command), \hyperpage{72}
3.102 + \item \isa {Ball} (constant), \hyperpage{103}
3.103 \item \isa {ballI} (theorem), \bold{102}
3.104 - \item \isa {best} (method), 86
3.105 - \item \isa {Bex} (constant), 103
3.106 + \item \isa {best} (method), \hyperpage{86}
3.107 + \item \isa {Bex} (constant), \hyperpage{103}
3.108 \item \isa {bexE} (theorem), \bold{102}
3.109 \item \isa {bexI} (theorem), \bold{102}
3.110 \item \isa {bij_def} (theorem), \bold{104}
3.111 - \item bijections, 104
3.112 - \item binary trees, 18
3.113 - \item binomial coefficients, 103
3.114 - \item bisimulations, 110
3.115 - \item \isa {blast} (method), 83--84, 86
3.116 - \item \isa {bool} (type), 4, 5
3.117 - \item boolean expressions example, 20--22
3.118 + \item bijections, \hyperpage{104}
3.119 + \item binary trees, \hyperpage{18}
3.120 + \item binomial coefficients, \hyperpage{103}
3.121 + \item bisimulations, \hyperpage{110}
3.122 + \item \isa {blast} (method), \hyperpage{83--84}, \hyperpage{86}
3.123 + \item \isa {bool} (type), \hyperpage{4, 5}
3.124 + \item boolean expressions example, \hyperpage{20--22}
3.125 \item \isa {bspec} (theorem), \bold{102}
3.126 - \item \isacommand{by} (command), 67
3.127 + \item \isacommand{by} (command), \hyperpage{67}
3.128
3.129 \indexspace
3.130
3.131 - \item \isa {card} (constant), 103
3.132 + \item \isa {card} (constant), \hyperpage{103}
3.133 \item \isa {card_Pow} (theorem), \bold{103}
3.134 \item \isa {card_Un_Int} (theorem), \bold{103}
3.135 - \item cardinality, 103
3.136 - \item \isa {case} (symbol), 32, 33
3.137 - \item \isa {case} expressions, 5, 6, 18
3.138 - \item case distinctions, 19
3.139 + \item cardinality, \hyperpage{103}
3.140 + \item \isa {case} (symbol), \hyperpage{32, 33}
3.141 + \item \isa {case} expressions, \hyperpage{5, 6}, \hyperpage{18}
3.142 + \item case distinctions, \hyperpage{19}
3.143 \item case splits, \bold{31}
3.144 - \item \isa {case_tac} (method), 19, 95, 151
3.145 - \item \isa {cases} (method), 156
3.146 - \item \isa {clarify} (method), 85, 86
3.147 - \item \isa {clarsimp} (method), 85, 86
3.148 + \item \isa {case_tac} (method), \hyperpage{19}, \hyperpage{95},
3.149 + \hyperpage{151}
3.150 + \item \isa {cases} (method), \hyperpage{156}
3.151 + \item \isa {clarify} (method), \hyperpage{85, 86}
3.152 + \item \isa {clarsimp} (method), \hyperpage{85, 86}
3.153 \item \isa {classical} (theorem), \bold{67}
3.154 \item coinduction, \bold{110}
3.155 - \item \isa {Collect} (constant), 103
3.156 - \item compiling expressions example, 36--38
3.157 + \item \isa {Collect} (constant), \hyperpage{103}
3.158 + \item compiling expressions example, \hyperpage{36--38}
3.159 \item \isa {Compl_iff} (theorem), \bold{100}
3.160 \item complement
3.161 - \subitem of a set, 99
3.162 + \subitem of a set, \hyperpage{99}
3.163 \item composition
3.164 \subitem of functions, \bold{104}
3.165 \subitem of relations, \bold{106}
3.166 \item conclusion
3.167 - \subitem of subgoal, 12
3.168 + \subitem of subgoal, \hyperpage{12}
3.169 \item conditional expressions, \see{\isa{if} expressions}{1}
3.170 - \item conditional simplification rules, 31
3.171 - \item \isa {cong} (attribute), 170
3.172 + \item conditional simplification rules, \hyperpage{31}
3.173 + \item \isa {cong} (attribute), \hyperpage{170}
3.174 \item congruence rules, \bold{169}
3.175 \item \isa {conjE} (theorem), \bold{65}
3.176 \item \isa {conjI} (theorem), \bold{62}
3.177 - \item \isa {Cons} (constant), 9
3.178 - \item \isacommand {constdefs} (command), 25
3.179 - \item \isacommand {consts} (command), 10
3.180 - \item contrapositives, 67
3.181 + \item \isa {Cons} (constant), \hyperpage{9}
3.182 + \item \isacommand {constdefs} (command), \hyperpage{25}
3.183 + \item \isacommand {consts} (command), \hyperpage{10}
3.184 + \item contrapositives, \hyperpage{67}
3.185 \item converse
3.186 \subitem of a relation, \bold{106}
3.187 \item \isa {converse_iff} (theorem), \bold{106}
3.188 - \item CTL, 115--120, 185--187
3.189 + \item CTL, \hyperpage{115--120}, \hyperpage{185--187}
3.190
3.191 \indexspace
3.192
3.193 - \item \isacommand {datatype} (command), 9, 38--43
3.194 - \item datatypes, 17--22
3.195 - \subitem and nested recursion, 40, 44
3.196 - \subitem mutually recursive, 38
3.197 - \subitem nested, 174
3.198 - \item \isacommand {defer} (command), 16, 94
3.199 - \item Definitional Approach, 26
3.200 + \item \isacommand {datatype} (command), \hyperpage{9},
3.201 + \hyperpage{38--43}
3.202 + \item datatypes, \hyperpage{17--22}
3.203 + \subitem and nested recursion, \hyperpage{40}, \hyperpage{44}
3.204 + \subitem mutually recursive, \hyperpage{38}
3.205 + \subitem nested, \hyperpage{174}
3.206 + \item \isacommand {defer} (command), \hyperpage{16}, \hyperpage{94}
3.207 + \item Definitional Approach, \hyperpage{26}
3.208 \item definitions, \bold{25}
3.209 \subitem unfolding, \bold{30}
3.210 - \item \isacommand {defs} (command), 25
3.211 - \item \isa {del} (modifier), 29
3.212 - \item description operators, 79--81
3.213 + \item \isacommand {defs} (command), \hyperpage{25}
3.214 + \item \isa {del} (modifier), \hyperpage{29}
3.215 + \item description operators, \hyperpage{79--81}
3.216 \item descriptions
3.217 - \subitem definite, 79
3.218 - \subitem indefinite, 80
3.219 - \item \isa {dest} (attribute), 96
3.220 - \item destruction rules, 65
3.221 + \subitem definite, \hyperpage{79}
3.222 + \subitem indefinite, \hyperpage{80}
3.223 + \item \isa {dest} (attribute), \hyperpage{96}
3.224 + \item destruction rules, \hyperpage{65}
3.225 \item \isa {diff_mult_distrib} (theorem), \bold{145}
3.226 \item difference
3.227 \subitem of sets, \bold{100}
3.228 \item \isa {disjCI} (theorem), \bold{68}
3.229 \item \isa {disjE} (theorem), \bold{64}
3.230 - \item \isa {div} (symbol), 23
3.231 - \item divides relation, 78, 89, 95--98, 146
3.232 + \item \isa {div} (symbol), \hyperpage{23}
3.233 + \item divides relation, \hyperpage{78}, \hyperpage{89},
3.234 + \hyperpage{95--98}, \hyperpage{146}
3.235 \item division
3.236 - \subitem by negative numbers, 147
3.237 - \subitem by zero, 146
3.238 - \subitem for type \protect\isa{nat}, 145
3.239 + \subitem by negative numbers, \hyperpage{147}
3.240 + \subitem by zero, \hyperpage{146}
3.241 + \subitem for type \protect\isa{nat}, \hyperpage{145}
3.242 \item domain
3.243 - \subitem of a relation, 106
3.244 + \subitem of a relation, \hyperpage{106}
3.245 \item \isa {Domain_iff} (theorem), \bold{106}
3.246 - \item \isacommand {done} (command), 13
3.247 - \item \isa {drule_tac} (method), 70, 90
3.248 + \item \isacommand {done} (command), \hyperpage{13}
3.249 + \item \isa {drule_tac} (method), \hyperpage{70}, \hyperpage{90}
3.250 \item \isa {dvd_add} (theorem), \bold{146}
3.251 \item \isa {dvd_anti_sym} (theorem), \bold{146}
3.252 \item \isa {dvd_def} (theorem), \bold{146}
3.253
3.254 \indexspace
3.255
3.256 - \item \isa {elim!} (attribute), 125
3.257 - \item elimination rules, 63--64
3.258 - \item \isacommand {end} (command), 14
3.259 - \item \isa {Eps} (constant), 103
3.260 - \item equality, 5
3.261 + \item \isa {elim!} (attribute), \hyperpage{125}
3.262 + \item elimination rules, \hyperpage{63--64}
3.263 + \item \isacommand {end} (command), \hyperpage{14}
3.264 + \item \isa {Eps} (constant), \hyperpage{103}
3.265 + \item equality, \hyperpage{5}
3.266 \subitem of functions, \bold{103}
3.267 - \subitem of records, 155
3.268 + \subitem of records, \hyperpage{155}
3.269 \subitem of sets, \bold{100}
3.270 \item \isa {equalityE} (theorem), \bold{100}
3.271 \item \isa {equalityI} (theorem), \bold{100}
3.272 - \item \isa {erule} (method), 64
3.273 - \item \isa {erule_tac} (method), 70
3.274 - \item Euclid's algorithm, 95--98
3.275 + \item \isa {erule} (method), \hyperpage{64}
3.276 + \item \isa {erule_tac} (method), \hyperpage{70}
3.277 + \item Euclid's algorithm, \hyperpage{95--98}
3.278 \item even numbers
3.279 - \subitem defining inductively, 121--125
3.280 + \subitem defining inductively, \hyperpage{121--125}
3.281 \item \texttt {EX}, \bold{203}
3.282 - \item \isa {Ex} (constant), 103
3.283 + \item \isa {Ex} (constant), \hyperpage{103}
3.284 \item \isa {exE} (theorem), \bold{76}
3.285 \item \isa {exI} (theorem), \bold{76}
3.286 \item \isa {ext} (theorem), \bold{103}
3.287 - \item \isa {extend} (constant), 157
3.288 + \item \isa {extend} (constant), \hyperpage{157}
3.289 \item extensionality
3.290 \subitem for functions, \bold{103, 104}
3.291 - \subitem for records, 155
3.292 + \subitem for records, \hyperpage{155}
3.293 \subitem for sets, \bold{100}
3.294 \item \ttEXU, \bold{203}
3.295
3.296 \indexspace
3.297
3.298 - \item \isa {False} (constant), 5
3.299 - \item \isa {fast} (method), 86, 118
3.300 - \item Fibonacci function, 47
3.301 - \item \isa {fields} (constant), 157
3.302 - \item \isa {finite} (symbol), 103
3.303 - \item \isa {Finites} (constant), 103
3.304 - \item fixed points, 110
3.305 - \item flags, 5, 6, 33
3.306 - \subitem setting and resetting, 5
3.307 - \item \isa {force} (method), 85, 86
3.308 - \item formulae, 5--6
3.309 - \item forward proof, 86--92
3.310 - \item \isa {frule} (method), 77
3.311 - \item \isa {frule_tac} (method), 70
3.312 - \item \isa {fst} (constant), 24
3.313 - \item function types, 5
3.314 - \item functions, 103--105
3.315 - \subitem partial, 176
3.316 - \subitem total, 11, 46--52
3.317 - \subitem underdefined, 177
3.318 + \item \isa {False} (constant), \hyperpage{5}
3.319 + \item \isa {fast} (method), \hyperpage{86}, \hyperpage{118}
3.320 + \item Fibonacci function, \hyperpage{47}
3.321 + \item \isa {fields} (constant), \hyperpage{157}
3.322 + \item \isa {finite} (symbol), \hyperpage{103}
3.323 + \item \isa {Finites} (constant), \hyperpage{103}
3.324 + \item fixed points, \hyperpage{110}
3.325 + \item flags, \hyperpage{5, 6}, \hyperpage{33}
3.326 + \subitem setting and resetting, \hyperpage{5}
3.327 + \item \isa {force} (method), \hyperpage{85, 86}
3.328 + \item formulae, \hyperpage{5--6}
3.329 + \item forward proof, \hyperpage{86--92}
3.330 + \item \isa {frule} (method), \hyperpage{77}
3.331 + \item \isa {frule_tac} (method), \hyperpage{70}
3.332 + \item \isa {fst} (constant), \hyperpage{24}
3.333 + \item function types, \hyperpage{5}
3.334 + \item functions, \hyperpage{103--105}
3.335 + \subitem partial, \hyperpage{176}
3.336 + \subitem total, \hyperpage{11}, \hyperpage{46--52}
3.337 + \subitem underdefined, \hyperpage{177}
3.338
3.339 \indexspace
3.340
3.341 - \item \isa {gcd} (constant), 87--88, 95--98
3.342 - \item generalizing for induction, 123
3.343 - \item generalizing induction formulae, 35
3.344 + \item \isa {gcd} (constant), \hyperpage{87--88}, \hyperpage{95--98}
3.345 + \item generalizing for induction, \hyperpage{123}
3.346 + \item generalizing induction formulae, \hyperpage{35}
3.347 \item Girard, Jean-Yves, \fnote{65}
3.348 - \item Gordon, Mike, 3
3.349 + \item Gordon, Mike, \hyperpage{3}
3.350 \item grammars
3.351 - \subitem defining inductively, 134--139
3.352 - \item ground terms example, 129--134
3.353 + \subitem defining inductively, \hyperpage{134--139}
3.354 + \item ground terms example, \hyperpage{129--134}
3.355
3.356 \indexspace
3.357
3.358 - \item \isa {hd} (constant), 17, 37
3.359 - \item Hilbert's $\varepsilon$-operator, 80
3.360 - \item HOLCF, 43
3.361 - \item Hopcroft, J. E., 139
3.362 - \item \isa {hypreal} (type), 149
3.363 + \item \isa {hd} (constant), \hyperpage{17}, \hyperpage{37}
3.364 + \item Hilbert's $\varepsilon$-operator, \hyperpage{80}
3.365 + \item HOLCF, \hyperpage{43}
3.366 + \item Hopcroft, J. E., \hyperpage{139}
3.367 + \item \isa {hypreal} (type), \hyperpage{149}
3.368
3.369 \indexspace
3.370
3.371 @@ -253,11 +257,12 @@
3.372 \subitem qualified, \bold{4}
3.373 \item identity function, \bold{104}
3.374 \item identity relation, \bold{106}
3.375 - \item \isa {if} expressions, 5, 6
3.376 - \subitem simplification of, 33
3.377 - \subitem splitting of, 31, 49
3.378 - \item if-and-only-if, 6
3.379 - \item \isa {iff} (attribute), 84, 96, 124
3.380 + \item \isa {if} expressions, \hyperpage{5, 6}
3.381 + \subitem simplification of, \hyperpage{33}
3.382 + \subitem splitting of, \hyperpage{31}, \hyperpage{49}
3.383 + \item if-and-only-if, \hyperpage{6}
3.384 + \item \isa {iff} (attribute), \hyperpage{84}, \hyperpage{96},
3.385 + \hyperpage{124}
3.386 \item \isa {iffD1} (theorem), \bold{88}
3.387 \item \isa {iffD2} (theorem), \bold{88}
3.388 \item image
3.389 @@ -266,383 +271,391 @@
3.390 \item \isa {image_def} (theorem), \bold{105}
3.391 \item \isa {Image_iff} (theorem), \bold{106}
3.392 \item \isa {impI} (theorem), \bold{66}
3.393 - \item implication, 66--67
3.394 - \item \isa {ind_cases} (method), 125
3.395 - \item \isa {induct_tac} (method), 12, 19, 52, 184
3.396 - \item induction, 180--187
3.397 - \subitem complete, 182
3.398 - \subitem deriving new schemas, 184
3.399 - \subitem on a term, 181
3.400 - \subitem recursion, 51--52
3.401 - \subitem structural, 19
3.402 - \subitem well-founded, 109
3.403 - \item induction heuristics, 34--36
3.404 - \item \isacommand {inductive} (command), 121
3.405 + \item implication, \hyperpage{66--67}
3.406 + \item \isa {ind_cases} (method), \hyperpage{125}
3.407 + \item \isa {induct_tac} (method), \hyperpage{12}, \hyperpage{19},
3.408 + \hyperpage{52}, \hyperpage{184}
3.409 + \item induction, \hyperpage{180--187}
3.410 + \subitem complete, \hyperpage{182}
3.411 + \subitem deriving new schemas, \hyperpage{184}
3.412 + \subitem on a term, \hyperpage{181}
3.413 + \subitem recursion, \hyperpage{51--52}
3.414 + \subitem structural, \hyperpage{19}
3.415 + \subitem well-founded, \hyperpage{109}
3.416 + \item induction heuristics, \hyperpage{34--36}
3.417 + \item \isacommand {inductive} (command), \hyperpage{121}
3.418 \item inductive definition
3.419 - \subitem simultaneous, 135
3.420 - \item inductive definitions, 121--139
3.421 - \item \isacommand {inductive\_cases} (command), 125, 133
3.422 - \item infinitely branching trees, 43
3.423 + \subitem simultaneous, \hyperpage{135}
3.424 + \item inductive definitions, \hyperpage{121--139}
3.425 + \item \isacommand {inductive\_cases} (command), \hyperpage{125},
3.426 + \hyperpage{133}
3.427 + \item infinitely branching trees, \hyperpage{43}
3.428 \item infix annotations, \bold{54}
3.429 - \item \isacommand{infixr} (annotation), 10
3.430 + \item \isacommand{infixr} (annotation), \hyperpage{10}
3.431 \item \isa {inj_on_def} (theorem), \bold{104}
3.432 - \item injections, 104
3.433 - \item \isa {insert} (constant), 101
3.434 - \item \isa {insert} (method), 91--92
3.435 + \item injections, \hyperpage{104}
3.436 + \item \isa {insert} (constant), \hyperpage{101}
3.437 + \item \isa {insert} (method), \hyperpage{91--92}
3.438 \item instance, \bold{160}
3.439 \item \texttt {INT}, \bold{203}
3.440 \item \texttt {Int}, \bold{203}
3.441 - \item \isa {int} (type), 147--148
3.442 + \item \isa {int} (type), \hyperpage{147--148}
3.443 \item \isa {INT_iff} (theorem), \bold{102}
3.444 \item \isa {IntD1} (theorem), \bold{99}
3.445 \item \isa {IntD2} (theorem), \bold{99}
3.446 - \item integers, 147--148
3.447 - \item \isa {INTER} (constant), 103
3.448 + \item integers, \hyperpage{147--148}
3.449 + \item \isa {INTER} (constant), \hyperpage{103}
3.450 \item \texttt {Inter}, \bold{203}
3.451 \item \isa {Inter_iff} (theorem), \bold{102}
3.452 - \item intersection, 99
3.453 - \subitem indexed, 102
3.454 + \item intersection, \hyperpage{99}
3.455 + \subitem indexed, \hyperpage{102}
3.456 \item \isa {IntI} (theorem), \bold{99}
3.457 - \item \isa {intro} (method), 68
3.458 - \item \isa {intro!} (attribute), 122
3.459 - \item \isa {intro_classes} (method), 160
3.460 - \item introduction rules, 62--63
3.461 - \item \isa {inv} (constant), 80
3.462 + \item \isa {intro} (method), \hyperpage{68}
3.463 + \item \isa {intro!} (attribute), \hyperpage{122}
3.464 + \item \isa {intro_classes} (method), \hyperpage{160}
3.465 + \item introduction rules, \hyperpage{62--63}
3.466 + \item \isa {inv} (constant), \hyperpage{80}
3.467 \item \isa {inv_image_def} (theorem), \bold{109}
3.468 \item inverse
3.469 \subitem of a function, \bold{104}
3.470 \subitem of a relation, \bold{106}
3.471 \item inverse image
3.472 - \subitem of a function, 105
3.473 - \subitem of a relation, 108
3.474 - \item \isa {itrev} (constant), 34
3.475 + \subitem of a function, \hyperpage{105}
3.476 + \subitem of a relation, \hyperpage{108}
3.477 + \item \isa {itrev} (constant), \hyperpage{34}
3.478
3.479 \indexspace
3.480
3.481 - \item \isacommand {kill} (command), 16
3.482 + \item \isacommand {kill} (command), \hyperpage{16}
3.483
3.484 \indexspace
3.485
3.486 - \item $\lambda$ expressions, 5
3.487 - \item LCF, 43
3.488 - \item \isa {LEAST} (symbol), 23, 79
3.489 + \item $\lambda$ expressions, \hyperpage{5}
3.490 + \item LCF, \hyperpage{43}
3.491 + \item \isa {LEAST} (symbol), \hyperpage{23}, \hyperpage{79}
3.492 \item least number operator, \see{\protect\isa{LEAST}}{79}
3.493 - \item Leibniz, Gottfried Wilhelm, 53
3.494 - \item \isacommand {lemma} (command), 13
3.495 - \item \isacommand {lemmas} (command), 87, 96
3.496 - \item \isa {length} (symbol), 18
3.497 + \item Leibniz, Gottfried Wilhelm, \hyperpage{53}
3.498 + \item \isacommand {lemma} (command), \hyperpage{13}
3.499 + \item \isacommand {lemmas} (command), \hyperpage{87}, \hyperpage{96}
3.500 + \item \isa {length} (symbol), \hyperpage{18}
3.501 \item \isa {length_induct}, \bold{184}
3.502 - \item \isa {less_than} (constant), 108
3.503 + \item \isa {less_than} (constant), \hyperpage{108}
3.504 \item \isa {less_than_iff} (theorem), \bold{108}
3.505 - \item \isa {let} expressions, 5, 6, 31
3.506 - \item \isa {Let_def} (theorem), 31
3.507 + \item \isa {let} expressions, \hyperpage{5, 6}, \hyperpage{31}
3.508 + \item \isa {Let_def} (theorem), \hyperpage{31}
3.509 \item \isa {lex_prod_def} (theorem), \bold{109}
3.510 - \item lexicographic product, \bold{109}, 172
3.511 + \item lexicographic product, \bold{109}, \hyperpage{172}
3.512 \item {\texttt{lfp}}
3.513 \subitem applications of, \see{CTL}{110}
3.514 - \item Library, 4
3.515 - \item linear arithmetic, 22--24, 143
3.516 - \item \isa {List} (theory), 17
3.517 - \item \isa {list} (type), 5, 9, 17
3.518 - \item \isa {list.split} (theorem), 32
3.519 + \item Library, \hyperpage{4}
3.520 + \item linear arithmetic, \hyperpage{22--24}, \hyperpage{143}
3.521 + \item \isa {List} (theory), \hyperpage{17}
3.522 + \item \isa {list} (type), \hyperpage{5}, \hyperpage{9},
3.523 + \hyperpage{17}
3.524 + \item \isa {list.split} (theorem), \hyperpage{32}
3.525 \item \isa {lists_mono} (theorem), \bold{131}
3.526 - \item Lowe, Gavin, 190--191
3.527 + \item Lowe, Gavin, \hyperpage{190--191}
3.528
3.529 \indexspace
3.530
3.531 - \item \isa {Main} (theory), 4
3.532 + \item \isa {Main} (theory), \hyperpage{4}
3.533 \item major premise, \bold{69}
3.534 - \item \isa {make} (constant), 157
3.535 - \item \isa {max} (constant), 23, 24
3.536 - \item measure functions, 47, 108
3.537 + \item \isa {make} (constant), \hyperpage{157}
3.538 + \item \isa {max} (constant), \hyperpage{23, 24}
3.539 + \item measure functions, \hyperpage{47}, \hyperpage{108}
3.540 \item \isa {measure_def} (theorem), \bold{109}
3.541 \item meta-logic, \bold{74}
3.542 \item methods, \bold{16}
3.543 - \item \isa {min} (constant), 23, 24
3.544 + \item \isa {min} (constant), \hyperpage{23, 24}
3.545 \item mixfix annotations, \bold{53}
3.546 - \item \isa {mod} (symbol), 23
3.547 + \item \isa {mod} (symbol), \hyperpage{23}
3.548 \item \isa {mod_div_equality} (theorem), \bold{145}
3.549 \item \isa {mod_mult_distrib} (theorem), \bold{145}
3.550 - \item model checking example, 110--120
3.551 - \item \emph{modus ponens}, 61, 66
3.552 + \item model checking example, \hyperpage{110--120}
3.553 + \item \emph{modus ponens}, \hyperpage{61}, \hyperpage{66}
3.554 \item \isa {mono_def} (theorem), \bold{110}
3.555 - \item monotone functions, \bold{110}, 133
3.556 - \subitem and inductive definitions, 131--132
3.557 - \item \isa {more} (constant), 152, 154
3.558 + \item monotone functions, \bold{110}, \hyperpage{133}
3.559 + \subitem and inductive definitions, \hyperpage{131--132}
3.560 + \item \isa {more} (constant), \hyperpage{152}, \hyperpage{154}
3.561 \item \isa {mp} (theorem), \bold{66}
3.562 - \item \isa {mult_ac} (theorems), 146
3.563 + \item \isa {mult_ac} (theorems), \hyperpage{146}
3.564 \item multiple inheritance, \bold{163}
3.565 \item multiset ordering, \bold{109}
3.566
3.567 \indexspace
3.568
3.569 - \item \isa {nat} (type), 4, 22, 145--147
3.570 - \item \isa {nat_less_induct} (theorem), 182
3.571 - \item natural deduction, 61--62
3.572 - \item natural numbers, 22, 145--147
3.573 - \item Needham-Schroeder protocol, 189--191
3.574 - \item negation, 67--69
3.575 - \item \isa {Nil} (constant), 9
3.576 - \item \isa {no_asm} (modifier), 29
3.577 - \item \isa {no_asm_simp} (modifier), 30
3.578 - \item \isa {no_asm_use} (modifier), 30
3.579 - \item non-standard reals, 149
3.580 + \item \isa {nat} (type), \hyperpage{4}, \hyperpage{22},
3.581 + \hyperpage{145--147}
3.582 + \item \isa {nat_less_induct} (theorem), \hyperpage{182}
3.583 + \item natural deduction, \hyperpage{61--62}
3.584 + \item natural numbers, \hyperpage{22}, \hyperpage{145--147}
3.585 + \item Needham-Schroeder protocol, \hyperpage{189--191}
3.586 + \item negation, \hyperpage{67--69}
3.587 + \item \isa {Nil} (constant), \hyperpage{9}
3.588 + \item \isa {no_asm} (modifier), \hyperpage{29}
3.589 + \item \isa {no_asm_simp} (modifier), \hyperpage{30}
3.590 + \item \isa {no_asm_use} (modifier), \hyperpage{30}
3.591 + \item non-standard reals, \hyperpage{149}
3.592 \item \isa {None} (constant), \bold{24}
3.593 \item \isa {notE} (theorem), \bold{67}
3.594 \item \isa {notI} (theorem), \bold{67}
3.595 - \item numbers, 143--149
3.596 - \item numeric literals, 144
3.597 - \subitem for type \protect\isa{nat}, 145
3.598 - \subitem for type \protect\isa{real}, 149
3.599 + \item numbers, \hyperpage{143--149}
3.600 + \item numeric literals, \hyperpage{144}
3.601 + \subitem for type \protect\isa{nat}, \hyperpage{145}
3.602 + \subitem for type \protect\isa{real}, \hyperpage{149}
3.603
3.604 \indexspace
3.605
3.606 - \item \isa {O} (symbol), 106
3.607 + \item \isa {O} (symbol), \hyperpage{106}
3.608 \item \texttt {o}, \bold{203}
3.609 \item \isa {o_def} (theorem), \bold{104}
3.610 - \item \isa {OF} (attribute), 89--90
3.611 - \item \isa {of} (attribute), 87, 90
3.612 - \item \isa {only} (modifier), 29
3.613 - \item \isacommand {oops} (command), 13
3.614 + \item \isa {OF} (attribute), \hyperpage{89--90}
3.615 + \item \isa {of} (attribute), \hyperpage{87}, \hyperpage{90}
3.616 + \item \isa {only} (modifier), \hyperpage{29}
3.617 + \item \isacommand {oops} (command), \hyperpage{13}
3.618 \item \isa {option} (type), \bold{24}
3.619 \item ordered rewriting, \bold{170}
3.620 - \item overloading, 23, 159--161
3.621 - \subitem and arithmetic, 144
3.622 + \item overloading, \hyperpage{23}, \hyperpage{159--161}
3.623 + \subitem and arithmetic, \hyperpage{144}
3.624
3.625 \indexspace
3.626
3.627 - \item pairs and tuples, 24, 149--152
3.628 + \item pairs and tuples, \hyperpage{24}, \hyperpage{149--152}
3.629 \item parent theories, \bold{4}
3.630 \item pattern matching
3.631 - \subitem and \isacommand{recdef}, 47
3.632 + \subitem and \isacommand{recdef}, \hyperpage{47}
3.633 \item patterns
3.634 \subitem higher-order, \bold{171}
3.635 - \item PDL, 112--114
3.636 - \item \isacommand {pr} (command), 16, 94
3.637 - \item \isacommand {prefer} (command), 16, 94
3.638 + \item PDL, \hyperpage{112--114}
3.639 + \item \isacommand {pr} (command), \hyperpage{16}, \hyperpage{94}
3.640 + \item \isacommand {prefer} (command), \hyperpage{16}, \hyperpage{94}
3.641 \item prefix annotation, \bold{56}
3.642 \item primitive recursion, \see{recursion, primitive}{1}
3.643 - \item \isacommand {primrec} (command), 10, 18, 38--43
3.644 - \item print mode, 55
3.645 - \item \isacommand {print\_syntax} (command), 54
3.646 + \item \isacommand {primrec} (command), \hyperpage{10}, \hyperpage{18},
3.647 + \hyperpage{38--43}
3.648 + \item print mode, \hyperpage{55}
3.649 + \item \isacommand {print\_syntax} (command), \hyperpage{54}
3.650 \item product type, \see{pairs and tuples}{1}
3.651 \item Proof General, \bold{7}
3.652 - \item proof state, 12
3.653 + \item proof state, \hyperpage{12}
3.654 \item proofs
3.655 \subitem abandoning, \bold{13}
3.656 - \subitem examples of failing, 81--83
3.657 + \subitem examples of failing, \hyperpage{81--83}
3.658 \item protocols
3.659 - \subitem security, 189--199
3.660 + \subitem security, \hyperpage{189--199}
3.661
3.662 \indexspace
3.663
3.664 - \item quantifiers, 6
3.665 - \subitem and inductive definitions, 129--131
3.666 - \subitem existential, 76
3.667 - \subitem for sets, 102
3.668 - \subitem instantiating, 78
3.669 - \subitem universal, 73--76
3.670 + \item quantifiers, \hyperpage{6}
3.671 + \subitem and inductive definitions, \hyperpage{129--131}
3.672 + \subitem existential, \hyperpage{76}
3.673 + \subitem for sets, \hyperpage{102}
3.674 + \subitem instantiating, \hyperpage{78}
3.675 + \subitem universal, \hyperpage{73--76}
3.676
3.677 \indexspace
3.678
3.679 \item \isa {r_into_rtrancl} (theorem), \bold{106}
3.680 \item \isa {r_into_trancl} (theorem), \bold{107}
3.681 \item range
3.682 - \subitem of a function, 105
3.683 - \subitem of a relation, 106
3.684 - \item \isa {range} (symbol), 105
3.685 + \subitem of a function, \hyperpage{105}
3.686 + \subitem of a relation, \hyperpage{106}
3.687 + \item \isa {range} (symbol), \hyperpage{105}
3.688 \item \isa {Range_iff} (theorem), \bold{106}
3.689 - \item \isa {Real} (theory), 149
3.690 - \item \isa {real} (type), 148--149
3.691 - \item real numbers, 148--149
3.692 - \item \isacommand {recdef} (command), 46--52, 108, 172--180
3.693 - \subitem and numeric literals, 144
3.694 - \item \isa {recdef_cong} (attribute), 176
3.695 - \item \isa {recdef_simp} (attribute), 49
3.696 - \item \isa {recdef_wf} (attribute), 174
3.697 - \item \isacommand {record} (command), 153
3.698 - \item records, 152--158
3.699 - \subitem extensible, 154--155
3.700 + \item \isa {Real} (theory), \hyperpage{149}
3.701 + \item \isa {real} (type), \hyperpage{148--149}
3.702 + \item real numbers, \hyperpage{148--149}
3.703 + \item \isacommand {recdef} (command), \hyperpage{46--52},
3.704 + \hyperpage{108}, \hyperpage{172--180}
3.705 + \subitem and numeric literals, \hyperpage{144}
3.706 + \item \isa {recdef_cong} (attribute), \hyperpage{176}
3.707 + \item \isa {recdef_simp} (attribute), \hyperpage{49}
3.708 + \item \isa {recdef_wf} (attribute), \hyperpage{174}
3.709 + \item \isacommand {record} (command), \hyperpage{153}
3.710 + \item records, \hyperpage{152--158}
3.711 + \subitem extensible, \hyperpage{154--155}
3.712 \item recursion
3.713 - \subitem guarded, 177
3.714 - \subitem primitive, 18
3.715 + \subitem guarded, \hyperpage{177}
3.716 + \subitem primitive, \hyperpage{18}
3.717 \subitem well-founded, \bold{173}
3.718 - \item recursion induction, 51--52
3.719 - \item \isacommand {redo} (command), 16
3.720 - \item reflexive and transitive closure, 106--108
3.721 + \item recursion induction, \hyperpage{51--52}
3.722 + \item \isacommand {redo} (command), \hyperpage{16}
3.723 + \item reflexive and transitive closure, \hyperpage{106--108}
3.724 \item reflexive transitive closure
3.725 - \subitem defining inductively, 126--129
3.726 + \subitem defining inductively, \hyperpage{126--129}
3.727 \item \isa {rel_comp_def} (theorem), \bold{106}
3.728 - \item relations, 105--108
3.729 - \subitem well-founded, 108--109
3.730 - \item \isa {rename_tac} (method), 76--77
3.731 - \item \isa {rev} (constant), 10--14, 34
3.732 + \item relations, \hyperpage{105--108}
3.733 + \subitem well-founded, \hyperpage{108--109}
3.734 + \item \isa {rename_tac} (method), \hyperpage{76--77}
3.735 + \item \isa {rev} (constant), \hyperpage{10--14}, \hyperpage{34}
3.736 \item rewrite rules, \bold{27}
3.737 \subitem permutative, \bold{170}
3.738 \item rewriting, \bold{27}
3.739 - \item \isa {rotate_tac} (method), 30
3.740 + \item \isa {rotate_tac} (method), \hyperpage{30}
3.741 \item \isa {rtrancl_refl} (theorem), \bold{106}
3.742 \item \isa {rtrancl_trans} (theorem), \bold{106}
3.743 - \item rule induction, 122--124
3.744 - \item rule inversion, 124--125, 133--134
3.745 - \item \isa {rule_format} (attribute), 181
3.746 - \item \isa {rule_tac} (method), 70
3.747 - \subitem and renaming, 77
3.748 + \item rule induction, \hyperpage{122--124}
3.749 + \item rule inversion, \hyperpage{124--125}, \hyperpage{133--134}
3.750 + \item \isa {rule_format} (attribute), \hyperpage{181}
3.751 + \item \isa {rule_tac} (method), \hyperpage{70}
3.752 + \subitem and renaming, \hyperpage{77}
3.753
3.754 \indexspace
3.755
3.756 - \item \isa {safe} (method), 85, 86
3.757 + \item \isa {safe} (method), \hyperpage{85, 86}
3.758 \item safe rules, \bold{84}
3.759 \item selector
3.760 - \subitem record, 153
3.761 - \item \isa {set} (type), 5, 99
3.762 - \item set comprehensions, 101--102
3.763 + \subitem record, \hyperpage{153}
3.764 + \item \isa {set} (type), \hyperpage{5}, \hyperpage{99}
3.765 + \item set comprehensions, \hyperpage{101--102}
3.766 \item \isa {set_ext} (theorem), \bold{100}
3.767 - \item sets, 99--103
3.768 - \subitem finite, 103
3.769 + \item sets, \hyperpage{99--103}
3.770 + \subitem finite, \hyperpage{103}
3.771 \subitem notation for finite, \bold{101}
3.772 \item settings, \see{flags}{1}
3.773 - \item \isa {show_brackets} (flag), 6
3.774 - \item \isa {show_types} (flag), 5, 16
3.775 - \item \isa {simp} (attribute), 11, 28
3.776 + \item \isa {show_brackets} (flag), \hyperpage{6}
3.777 + \item \isa {show_types} (flag), \hyperpage{5}, \hyperpage{16}
3.778 + \item \isa {simp} (attribute), \hyperpage{11}, \hyperpage{28}
3.779 \item \isa {simp} (method), \bold{28}
3.780 - \item \isa {simp} del (attribute), 28
3.781 - \item \isa {simp_all} (method), 29, 38
3.782 - \item simplification, 27--33, 169--172
3.783 - \subitem of \isa{let}-expressions, 31
3.784 - \subitem with definitions, 30
3.785 - \subitem with/of assumptions, 29
3.786 - \item simplification rule, 171--172
3.787 - \item simplification rules, 28
3.788 - \subitem adding and deleting, 29
3.789 - \item \isa {simplified} (attribute), 87, 90
3.790 - \item \isa {size} (constant), 17
3.791 - \item \isa {snd} (constant), 24
3.792 - \item \isa {SOME} (symbol), 80
3.793 + \item \isa {simp} del (attribute), \hyperpage{28}
3.794 + \item \isa {simp_all} (method), \hyperpage{29}, \hyperpage{38}
3.795 + \item simplification, \hyperpage{27--33}, \hyperpage{169--172}
3.796 + \subitem of \isa{let}-expressions, \hyperpage{31}
3.797 + \subitem with definitions, \hyperpage{30}
3.798 + \subitem with/of assumptions, \hyperpage{29}
3.799 + \item simplification rule, \hyperpage{171--172}
3.800 + \item simplification rules, \hyperpage{28}
3.801 + \subitem adding and deleting, \hyperpage{29}
3.802 + \item \isa {simplified} (attribute), \hyperpage{87}, \hyperpage{90}
3.803 + \item \isa {size} (constant), \hyperpage{17}
3.804 + \item \isa {snd} (constant), \hyperpage{24}
3.805 + \item \isa {SOME} (symbol), \hyperpage{80}
3.806 \item \texttt {SOME}, \bold{203}
3.807 \item \isa {Some} (constant), \bold{24}
3.808 \item \isa {some_equality} (theorem), \bold{80}
3.809 \item \isa {someI} (theorem), \bold{80}
3.810 \item \isa {someI2} (theorem), \bold{80}
3.811 \item \isa {someI_ex} (theorem), \bold{81}
3.812 - \item sorts, 164
3.813 + \item sorts, \hyperpage{164}
3.814 \item \isa {spec} (theorem), \bold{74}
3.815 - \item \isa {split} (attribute), 32
3.816 - \item \isa {split} (constant), 150
3.817 - \item \isa {split} (method), 31, 150
3.818 - \item \isa {split} (modifier), 32
3.819 + \item \isa {split} (attribute), \hyperpage{32}
3.820 + \item \isa {split} (constant), \hyperpage{150}
3.821 + \item \isa {split} (method), \hyperpage{31}, \hyperpage{150}
3.822 + \item \isa {split} (modifier), \hyperpage{32}
3.823 \item split rule, \bold{32}
3.824 - \item \isa {split_if} (theorem), 32
3.825 - \item \isa {split_if_asm} (theorem), 32
3.826 + \item \isa {split_if} (theorem), \hyperpage{32}
3.827 + \item \isa {split_if_asm} (theorem), \hyperpage{32}
3.828 \item \isa {ssubst} (theorem), \bold{71}
3.829 \item structural induction, \see{induction, structural}{1}
3.830 - \item subclasses, 158, 163
3.831 - \item subgoal numbering, 46
3.832 - \item \isa {subgoal_tac} (method), 92
3.833 - \item subgoals, 12
3.834 + \item subclasses, \hyperpage{158}, \hyperpage{163}
3.835 + \item subgoal numbering, \hyperpage{46}
3.836 + \item \isa {subgoal_tac} (method), \hyperpage{92}
3.837 + \item subgoals, \hyperpage{12}
3.838 \item subset relation, \bold{100}
3.839 \item \isa {subsetD} (theorem), \bold{100}
3.840 \item \isa {subsetI} (theorem), \bold{100}
3.841 - \item \isa {subst} (method), 71
3.842 - \item substitution, 71--73
3.843 - \item \isa {Suc} (constant), 22
3.844 + \item \isa {subst} (method), \hyperpage{71}
3.845 + \item substitution, \hyperpage{71--73}
3.846 + \item \isa {Suc} (constant), \hyperpage{22}
3.847 \item \isa {surj_def} (theorem), \bold{104}
3.848 - \item surjections, 104
3.849 + \item surjections, \hyperpage{104}
3.850 \item \isa {sym} (theorem), \bold{88}
3.851 \item symbols, \bold{55}
3.852 - \item syntax, 6, 11
3.853 - \item \isacommand {syntax} (command), 56
3.854 - \item syntax translations, 57
3.855 + \item syntax, \hyperpage{6}, \hyperpage{11}
3.856 + \item \isacommand {syntax} (command), \hyperpage{56}
3.857 + \item syntax translations, \hyperpage{57}
3.858
3.859 \indexspace
3.860
3.861 - \item tacticals, 93
3.862 - \item tactics, 12
3.863 - \item \isacommand {term} (command), 16
3.864 + \item tacticals, \hyperpage{93}
3.865 + \item tactics, \hyperpage{12}
3.866 + \item \isacommand {term} (command), \hyperpage{16}
3.867 \item term rewriting, \bold{27}
3.868 \item termination, \see{functions, total}{1}
3.869 - \item terms, 5
3.870 - \item \isa {THE} (symbol), 79
3.871 + \item terms, \hyperpage{5}
3.872 + \item \isa {THE} (symbol), \hyperpage{79}
3.873 \item \isa {the_equality} (theorem), \bold{79}
3.874 - \item \isa {THEN} (attribute), \bold{88}, 90, 96
3.875 - \item \isacommand {theorem} (command), \bold{11}, 13
3.876 - \item theories, 4
3.877 + \item \isa {THEN} (attribute), \bold{88}, \hyperpage{90},
3.878 + \hyperpage{96}
3.879 + \item \isacommand {theorem} (command), \bold{11}, \hyperpage{13}
3.880 + \item theories, \hyperpage{4}
3.881 \subitem abandoning, \bold{16}
3.882 - \item \isacommand {theory} (command), 16
3.883 - \item theory files, 4
3.884 - \item \isacommand {thm} (command), 16
3.885 - \item \isa {tl} (constant), 17
3.886 - \item \isa {ToyList} example, 9--14
3.887 - \item \isa {trace_simp} (flag), 33
3.888 + \item \isacommand {theory} (command), \hyperpage{16}
3.889 + \item theory files, \hyperpage{4}
3.890 + \item \isacommand {thm} (command), \hyperpage{16}
3.891 + \item \isa {tl} (constant), \hyperpage{17}
3.892 + \item \isa {ToyList} example, \hyperpage{9--14}
3.893 + \item \isa {trace_simp} (flag), \hyperpage{33}
3.894 \item tracing the simplifier, \bold{33}
3.895 \item \isa {trancl_trans} (theorem), \bold{107}
3.896 - \item transition systems, 111
3.897 - \item \isacommand {translations} (command), 57
3.898 - \item tries, 44--46
3.899 - \item \isa {True} (constant), 5
3.900 - \item \isa {truncate} (constant), 157
3.901 + \item transition systems, \hyperpage{111}
3.902 + \item \isacommand {translations} (command), \hyperpage{57}
3.903 + \item tries, \hyperpage{44--46}
3.904 + \item \isa {True} (constant), \hyperpage{5}
3.905 + \item \isa {truncate} (constant), \hyperpage{157}
3.906 \item tuples, \see{pairs and tuples}{1}
3.907 - \item \isacommand {typ} (command), 16
3.908 + \item \isacommand {typ} (command), \hyperpage{16}
3.909 \item type constraints, \bold{6}
3.910 - \item type constructors, 5
3.911 + \item type constructors, \hyperpage{5}
3.912 \item type inference, \bold{5}
3.913 - \item type synonyms, 25
3.914 - \item type variables, 5
3.915 - \item \isacommand {typedecl} (command), 111, 165
3.916 - \item \isacommand {typedef} (command), 165--168
3.917 - \item types, 4--5
3.918 - \subitem declaring, 165
3.919 - \subitem defining, 165--168
3.920 - \item \isacommand {types} (command), 25
3.921 + \item type synonyms, \hyperpage{25}
3.922 + \item type variables, \hyperpage{5}
3.923 + \item \isacommand {typedecl} (command), \hyperpage{111},
3.924 + \hyperpage{165}
3.925 + \item \isacommand {typedef} (command), \hyperpage{165--168}
3.926 + \item types, \hyperpage{4--5}
3.927 + \subitem declaring, \hyperpage{165}
3.928 + \subitem defining, \hyperpage{165--168}
3.929 + \item \isacommand {types} (command), \hyperpage{25}
3.930
3.931 \indexspace
3.932
3.933 - \item Ullman, J. D., 139
3.934 + \item Ullman, J. D., \hyperpage{139}
3.935 \item \texttt {UN}, \bold{203}
3.936 \item \texttt {Un}, \bold{203}
3.937 \item \isa {UN_E} (theorem), \bold{102}
3.938 \item \isa {UN_I} (theorem), \bold{102}
3.939 \item \isa {UN_iff} (theorem), \bold{102}
3.940 \item \isa {Un_subset_iff} (theorem), \bold{100}
3.941 - \item \isacommand {undo} (command), 16
3.942 + \item \isacommand {undo} (command), \hyperpage{16}
3.943 \item \isa {unfold} (method), \bold{31}
3.944 - \item Unicode, 55
3.945 - \item unification, 70--73
3.946 - \item \isa {UNION} (constant), 103
3.947 + \item Unicode, \hyperpage{55}
3.948 + \item unification, \hyperpage{70--73}
3.949 + \item \isa {UNION} (constant), \hyperpage{103}
3.950 \item \texttt {Union}, \bold{203}
3.951 \item union
3.952 - \subitem indexed, 102
3.953 + \subitem indexed, \hyperpage{102}
3.954 \item \isa {Union_iff} (theorem), \bold{102}
3.955 - \item \isa {unit} (type), 24
3.956 - \item unknowns, 7, \bold{62}
3.957 + \item \isa {unit} (type), \hyperpage{24}
3.958 + \item unknowns, \hyperpage{7}, \bold{62}
3.959 \item unsafe rules, \bold{84}
3.960 \item update
3.961 - \subitem record, 153
3.962 + \subitem record, \hyperpage{153}
3.963 \item updating a function, \bold{103}
3.964
3.965 \indexspace
3.966
3.967 - \item variables, 7
3.968 - \subitem schematic, 7
3.969 - \subitem type, 5
3.970 + \item variables, \hyperpage{7}
3.971 + \subitem schematic, \hyperpage{7}
3.972 + \subitem type, \hyperpage{5}
3.973 \item \isa {vimage_def} (theorem), \bold{105}
3.974
3.975 \indexspace
3.976
3.977 - \item Wenzel, Markus, vii
3.978 + \item Wenzel, Markus, \hyperpage{vii}
3.979 \item \isa {wf_induct} (theorem), \bold{109}
3.980 \item \isa {wf_inv_image} (theorem), \bold{109}
3.981 \item \isa {wf_less_than} (theorem), \bold{108}
3.982 \item \isa {wf_lex_prod} (theorem), \bold{109}
3.983 \item \isa {wf_measure} (theorem), \bold{109}
3.984 - \item \isa {wf_subset} (theorem), 174
3.985 - \item \isa {while} (constant), 179
3.986 - \item \isa {While_Combinator} (theory), 179
3.987 - \item \isa {while_rule} (theorem), 179
3.988 + \item \isa {wf_subset} (theorem), \hyperpage{174}
3.989 + \item \isa {while} (constant), \hyperpage{179}
3.990 + \item \isa {While_Combinator} (theory), \hyperpage{179}
3.991 + \item \isa {while_rule} (theorem), \hyperpage{179}
3.992
3.993 \indexspace
3.994
3.995 - \item \isa {zadd_ac} (theorems), 147
3.996 - \item \isa {zmult_ac} (theorems), 147
3.997 + \item \isa {zadd_ac} (theorems), \hyperpage{147}
3.998 + \item \isa {zmult_ac} (theorems), \hyperpage{147}
3.999
3.1000 \end{theindex}