*** empty log message ***
authorwenzelm
Fri Jul 20 17:49:21 2001 +0200 (2001-07-20)
changeset 114312328d48eeba8
parent 11430 c51de60e26cf
child 11432 8a203ae6efe3
*** empty log message ***
doc-src/TutorialI/tutorial.ind
     1.1 --- a/doc-src/TutorialI/tutorial.ind	Fri Jul 20 17:49:10 2001 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.ind	Fri Jul 20 17:49:21 2001 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4    \item \ttall, \bold{189}
     1.5    \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{189}
     1.6    \item \isasymexists, \bold{3}
     1.7 -  \item \texttt{?}, \hyperpage{5}, \bold{189}
     1.8 +  \item \texttt{?}, 5, \bold{189}
     1.9    \item \emph {$\varepsilon $}, \bold{189}
    1.10    \item \isasymuniqex, \bold{3}, \bold{189}
    1.11    \item \ttuniquex, \bold{189}
    1.12 @@ -13,7 +13,8 @@
    1.13    \item \isasymand, \bold{3}
    1.14    \item {\texttt {\&}}, \bold{189}
    1.15    \item \texttt {=}, \bold{3}
    1.16 -  \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{189}
    1.17 +  \item \emph {$\DOTSB \mathrel {\smash -}\mathrel {\mkern -3mu}\rightarrow $}, 
    1.18 +		\bold{189}
    1.19    \item \isasymimp, \bold{3}
    1.20    \item \texttt {-->}, \bold{189}
    1.21    \item \emph {$\neg $}, \bold{189}
    1.22 @@ -34,7 +35,7 @@
    1.23    \item \texttt {<}, \bold{20, 21}
    1.24    \item \texttt{[]}, \bold{7}
    1.25    \item \texttt{\#}, \bold{7}
    1.26 -  \item \texttt{\at}, \bold{8}, \hyperpage{189}
    1.27 +  \item \texttt{\at}, \bold{8}, 189
    1.28    \item \emph {$\in $}, \bold{189}
    1.29    \item \texttt {:}, \bold{189}
    1.30    \item \isasymnotin, \bold{189}
    1.31 @@ -59,7 +60,8 @@
    1.32    \item \emph {$\Rightarrow $}, \bold{3}, \bold{189}
    1.33    \item \texttt {=>}, \bold{189}
    1.34    \item \texttt {<=}, \bold{189}
    1.35 -  \item \emph {$\DOTSB \Relbar \joinrel \Rightarrow $}, \bold{189}
    1.36 +  \item \emph {$\DOTSB \mathrel =\mathrel {\mkern -3mu}\Rightarrow $}, 
    1.37 +		\bold{189}
    1.38    \item \texttt {==>}, \bold{189}
    1.39    \item \emph {$\mathopen {[\mkern -3mu[}$}, \bold{10}, \bold{189}
    1.40    \item \ttlbr, \bold{189}
    1.41 @@ -73,190 +75,187 @@
    1.42    \item \texttt {'a}, \bold{3}
    1.43    \item \texttt {()}, \bold{22}
    1.44    \item \texttt {::}, \bold{4}
    1.45 -  \item \isa {+} (tactical), \hyperpage{83}
    1.46 +  \item \isa {+} (tactical), 83
    1.47    \item \isa {<*lex*>}, \see{lexicographic product}{1}
    1.48 -  \item \isa {?} (tactical), \hyperpage{83}
    1.49 -  \item \texttt{|} (tactical), \hyperpage{83}
    1.50 +  \item \isa {?} (tactical), 83
    1.51 +  \item \texttt{|} (tactical), 83
    1.52  
    1.53    \indexspace
    1.54  
    1.55 -  \item \isa {0} (constant), \hyperpage{20, 21}, \hyperpage{133}
    1.56 -  \item \isa {1} (symbol), \hyperpage{133}
    1.57 -  \item \isa {2} (symbol), \hyperpage{133}
    1.58 +  \item \isa {0} (constant), 20, 21, 133
    1.59 +  \item \isa {1} (symbol), 133
    1.60 +  \item \isa {2} (symbol), 133
    1.61  
    1.62    \indexspace
    1.63  
    1.64    \item abandoning a proof, \bold{11}
    1.65    \item abandoning a theory, \bold{14}
    1.66 -  \item \isa {abs} (constant), \hyperpage{135}
    1.67 +  \item \isa {abs} (constant), 135
    1.68    \item \texttt {abs}, \bold{189}
    1.69 -  \item absolute value, \hyperpage{135}
    1.70 +  \item absolute value, 135
    1.71    \item \isa {add_assoc} (theorem), \bold{134}
    1.72    \item \isa {add_commute} (theorem), \bold{134}
    1.73    \item \isa {add_mult_distrib} (theorem), \bold{133}
    1.74    \item \texttt {ALL}, \bold{189}
    1.75 -  \item \isa {All} (constant), \hyperpage{93}
    1.76 +  \item \isa {All} (constant), 93
    1.77    \item \isa {allE} (theorem), \bold{65}
    1.78    \item \isa {allI} (theorem), \bold{64}
    1.79 -  \item \isacommand {apply} (command), \hyperpage{13}
    1.80 +  \item \isacommand {apply} (command), 13
    1.81    \item \isa {arg_cong} (theorem), \bold{80}
    1.82 -  \item \isa {arith} (method), \hyperpage{21}, \hyperpage{131}
    1.83 +  \item \isa {arith} (method), 21, 131
    1.84    \item \textsc {ascii} symbols, \bold{189}
    1.85 -  \item associative-commutative function, \hyperpage{158}
    1.86 -  \item \isa {assumption} (method), \hyperpage{53}
    1.87 +  \item associative-commutative function, 158
    1.88 +  \item \isa {assumption} (method), 53
    1.89    \item assumptions
    1.90 -    \subitem renaming, \hyperpage{66--67}
    1.91 -    \subitem reusing, \hyperpage{67}
    1.92 -  \item \isa {auto} (method), \hyperpage{36}, \hyperpage{76}
    1.93 -  \item \isa {axclass}, \hyperpage{144--150}
    1.94 -  \item axiom of choice, \hyperpage{70}
    1.95 -  \item axiomatic type classes, \hyperpage{144--150}
    1.96 +    \subitem renaming, 66--67
    1.97 +    \subitem reusing, 67
    1.98 +  \item \isa {auto} (method), 36, 76
    1.99 +  \item \isa {axclass}, 144--150
   1.100 +  \item axiom of choice, 70
   1.101 +  \item axiomatic type classes, 144--150
   1.102  
   1.103    \indexspace
   1.104  
   1.105 -  \item \isacommand {back} (command), \hyperpage{62}
   1.106 -  \item \isa {Ball} (constant), \hyperpage{93}
   1.107 +  \item \isacommand {back} (command), 62
   1.108 +  \item \isa {Ball} (constant), 93
   1.109    \item \isa {ballI} (theorem), \bold{92}
   1.110 -  \item \isa {best} (method), \hyperpage{75, 76}
   1.111 -  \item \isa {Bex} (constant), \hyperpage{93}
   1.112 +  \item \isa {best} (method), 75, 76
   1.113 +  \item \isa {Bex} (constant), 93
   1.114    \item \isa {bexE} (theorem), \bold{92}
   1.115    \item \isa {bexI} (theorem), \bold{92}
   1.116    \item \isa {bij_def} (theorem), \bold{94}
   1.117 -  \item bijections, \hyperpage{94}
   1.118 -  \item binomial coefficients, \hyperpage{93}
   1.119 -  \item bisimulations, \hyperpage{100}
   1.120 -  \item \isa {blast} (method), \hyperpage{72--75}
   1.121 -  \item \isa {bool} (type), \hyperpage{2, 3}
   1.122 +  \item bijections, 94
   1.123 +  \item binomial coefficients, 93
   1.124 +  \item bisimulations, 100
   1.125 +  \item \isa {blast} (method), 72--75
   1.126 +  \item \isa {bool} (type), 2, 3
   1.127    \item \isa {bspec} (theorem), \bold{92}
   1.128 -  \item \isacommand{by} (command), \hyperpage{57}
   1.129 +  \item \isacommand{by} (command), 57
   1.130  
   1.131    \indexspace
   1.132  
   1.133 -  \item \isa {card} (constant), \hyperpage{93}
   1.134 +  \item \isa {card} (constant), 93
   1.135    \item \isa {card_Pow} (theorem), \bold{93}
   1.136    \item \isa {card_Un_Int} (theorem), \bold{93}
   1.137 -  \item cardinality, \hyperpage{93}
   1.138 -  \item \isa {case} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{16}, 
   1.139 -		\hyperpage{30, 31}
   1.140 +  \item cardinality, 93
   1.141 +  \item \isa {case} (symbol), \bold{3}, 4, 16, 30, 31
   1.142    \item case distinction, \bold{17}
   1.143    \item case splits, \bold{29}
   1.144 -  \item \isa {case_tac} (method), \hyperpage{17}, \hyperpage{85}
   1.145 -  \item \isa {clarify} (method), \hyperpage{74}, \hyperpage{76}
   1.146 -  \item \isa {clarsimp} (method), \hyperpage{75, 76}
   1.147 +  \item \isa {case_tac} (method), 17, 85
   1.148 +  \item \isa {clarify} (method), 74, 76
   1.149 +  \item \isa {clarsimp} (method), 75, 76
   1.150    \item \isa {classical} (theorem), \bold{57}
   1.151    \item coinduction, \bold{100}
   1.152 -  \item \isa {Collect} (constant), \hyperpage{93}
   1.153 +  \item \isa {Collect} (constant), 93
   1.154    \item \isa {comp_def} (theorem), \bold{96}
   1.155    \item \isa {Compl_iff} (theorem), \bold{90}
   1.156    \item complement
   1.157 -    \subitem of a set, \hyperpage{89}
   1.158 +    \subitem of a set, 89
   1.159    \item composition
   1.160      \subitem of functions, \bold{94}
   1.161      \subitem of relations, \bold{96}
   1.162    \item congruence rules, \bold{157}
   1.163    \item \isa {conjE} (theorem), \bold{55}
   1.164    \item \isa {conjI} (theorem), \bold{52}
   1.165 -  \item \isa {Cons} (constant), \hyperpage{7}
   1.166 -  \item \isacommand {constdefs} (command), \hyperpage{23}
   1.167 -  \item contrapositives, \hyperpage{57}
   1.168 +  \item \isa {Cons} (constant), 7
   1.169 +  \item \isacommand {constdefs} (command), 23
   1.170 +  \item contrapositives, 57
   1.171    \item converse
   1.172      \subitem of a relation, \bold{96}
   1.173    \item \isa {converse_iff} (theorem), \bold{96}
   1.174 -  \item CTL, \hyperpage{100--110}
   1.175 +  \item CTL, 100--110
   1.176  
   1.177    \indexspace
   1.178  
   1.179 -  \item \isacommand {datatype} (command), \hyperpage{7}, 
   1.180 -		\hyperpage{36--42}
   1.181 -  \item \isacommand {defer} (command), \hyperpage{14}, \hyperpage{84}
   1.182 +  \item \isacommand {datatype} (command), 7, 36--42
   1.183 +  \item \isacommand {defer} (command), 14, 84
   1.184    \item definitions, \bold{23}
   1.185      \subitem unfolding, \bold{28}
   1.186 -  \item \isacommand {defs} (command), \hyperpage{23}
   1.187 +  \item \isacommand {defs} (command), 23
   1.188    \item descriptions
   1.189 -    \subitem definite, \hyperpage{69}
   1.190 -    \subitem indefinite, \hyperpage{70}
   1.191 -  \item \isa {dest} (attribute), \hyperpage{86}
   1.192 -  \item destruction rules, \hyperpage{55}
   1.193 +    \subitem definite, 69
   1.194 +    \subitem indefinite, 70
   1.195 +  \item \isa {dest} (attribute), 86
   1.196 +  \item destruction rules, 55
   1.197    \item \isa {diff_mult_distrib} (theorem), \bold{133}
   1.198    \item difference
   1.199      \subitem of sets, \bold{90}
   1.200    \item \isa {disjCI} (theorem), \bold{58}
   1.201    \item \isa {disjE} (theorem), \bold{54}
   1.202 -  \item \isa {div} (symbol), \hyperpage{20}
   1.203 -  \item divides relation, \hyperpage{68}, \hyperpage{78}, 
   1.204 -		\hyperpage{85--87}, \hyperpage{134}
   1.205 +  \item \isa {div} (symbol), 20
   1.206 +  \item divides relation, 68, 78, 85--87, 134
   1.207    \item division
   1.208 -    \subitem by negative numbers, \hyperpage{135}
   1.209 -    \subitem by zero, \hyperpage{134}
   1.210 -    \subitem for type \protect\isa{nat}, \hyperpage{133}
   1.211 +    \subitem by negative numbers, 135
   1.212 +    \subitem by zero, 134
   1.213 +    \subitem for type \protect\isa{nat}, 133
   1.214    \item domain
   1.215 -    \subitem of a relation, \hyperpage{96}
   1.216 +    \subitem of a relation, 96
   1.217    \item \isa {Domain_iff} (theorem), \bold{96}
   1.218 -  \item \isacommand {done} (command), \hyperpage{11}
   1.219 -  \item \isa {drule_tac} (method), \hyperpage{60}, \hyperpage{80}
   1.220 +  \item \isacommand {done} (command), 11
   1.221 +  \item \isa {drule_tac} (method), 60, 80
   1.222    \item \isa {dvd_add} (theorem), \bold{134}
   1.223    \item \isa {dvd_anti_sym} (theorem), \bold{134}
   1.224    \item \isa {dvd_def} (theorem), \bold{134}
   1.225  
   1.226    \indexspace
   1.227  
   1.228 -  \item \isa {elim!} (attribute), \hyperpage{115}
   1.229 -  \item elimination rules, \hyperpage{53--54}
   1.230 -  \item \isa {Eps} (constant), \hyperpage{93}
   1.231 +  \item \isa {elim!} (attribute), 115
   1.232 +  \item elimination rules, 53--54
   1.233 +  \item \isa {Eps} (constant), 93
   1.234    \item equality
   1.235      \subitem of functions, \bold{93}
   1.236 -    \subitem of records, \hyperpage{143}
   1.237 +    \subitem of records, 143
   1.238      \subitem of sets, \bold{90}
   1.239    \item \isa {equalityE} (theorem), \bold{90}
   1.240    \item \isa {equalityI} (theorem), \bold{90}
   1.241 -  \item \isa {erule} (method), \hyperpage{54}
   1.242 -  \item \isa {erule_tac} (method), \hyperpage{60}
   1.243 -  \item Euclid's algorithm, \hyperpage{85--87}
   1.244 +  \item \isa {erule} (method), 54
   1.245 +  \item \isa {erule_tac} (method), 60
   1.246 +  \item Euclid's algorithm, 85--87
   1.247    \item even numbers
   1.248 -    \subitem defining inductively, \hyperpage{111--115}
   1.249 +    \subitem defining inductively, 111--115
   1.250    \item \texttt {EX}, \bold{189}
   1.251 -  \item \isa {Ex} (constant), \hyperpage{93}
   1.252 +  \item \isa {Ex} (constant), 93
   1.253    \item \isa {exE} (theorem), \bold{66}
   1.254    \item \isa {exI} (theorem), \bold{66}
   1.255    \item \isa {ext} (theorem), \bold{93}
   1.256    \item extensionality
   1.257      \subitem for functions, \bold{93, 94}
   1.258 -    \subitem for records, \hyperpage{143}
   1.259 +    \subitem for records, 143
   1.260      \subitem for sets, \bold{90}
   1.261    \item \ttEXU, \bold{189}
   1.262  
   1.263    \indexspace
   1.264  
   1.265 -  \item \isa {False} (constant), \hyperpage{3}
   1.266 -  \item \isa {fast} (method), \hyperpage{75, 76}
   1.267 -  \item \isa {finite} (symbol), \hyperpage{93}
   1.268 -  \item \isa {Finites} (constant), \hyperpage{93}
   1.269 -  \item fixed points, \hyperpage{100}
   1.270 -  \item flags, \hyperpage{3, 4}, \hyperpage{31}
   1.271 -    \subitem setting and resetting, \hyperpage{3}
   1.272 -  \item \isa {force} (method), \hyperpage{75, 76}
   1.273 +  \item \isa {False} (constant), 3
   1.274 +  \item \isa {fast} (method), 75, 76
   1.275 +  \item \isa {finite} (symbol), 93
   1.276 +  \item \isa {Finites} (constant), 93
   1.277 +  \item fixed points, 100
   1.278 +  \item flags, 3, 4, 31
   1.279 +    \subitem setting and resetting, 3
   1.280 +  \item \isa {force} (method), 75, 76
   1.281    \item formulae, \bold{3}
   1.282 -  \item forward proof, \hyperpage{76--82}
   1.283 -  \item \isa {frule} (method), \hyperpage{67}
   1.284 -  \item \isa {frule_tac} (method), \hyperpage{60}
   1.285 -  \item \isa {fst} (constant), \hyperpage{21}
   1.286 -  \item functions, \hyperpage{93--95}
   1.287 -    \subitem total, \hyperpage{9}, \hyperpage{45--50}
   1.288 -    \subitem underdefined, \hyperpage{165}
   1.289 +  \item forward proof, 76--82
   1.290 +  \item \isa {frule} (method), 67
   1.291 +  \item \isa {frule_tac} (method), 60
   1.292 +  \item \isa {fst} (constant), 21
   1.293 +  \item functions, 93--95
   1.294 +    \subitem total, 9, 45--50
   1.295 +    \subitem underdefined, 165
   1.296  
   1.297    \indexspace
   1.298  
   1.299 -  \item \isa {gcd} (constant), \hyperpage{76--78}, \hyperpage{85--87}
   1.300 -  \item generalizing for induction, \hyperpage{113}
   1.301 +  \item \isa {gcd} (constant), 76--78, 85--87
   1.302 +  \item generalizing for induction, 113
   1.303    \item Girard, Jean-Yves, \fnote{55}
   1.304 -  \item ground terms example, \hyperpage{119--124}
   1.305 +  \item ground terms example, 119--124
   1.306  
   1.307    \indexspace
   1.308  
   1.309 -  \item \isa {hd} (constant), \hyperpage{15}
   1.310 +  \item \isa {hd} (constant), 15
   1.311    \item higher-order pattern, \bold{159}
   1.312 -  \item Hilbert's $\varepsilon$-operator, \hyperpage{69--71}
   1.313 -  \item \isa {hypreal} (type), \hyperpage{137}
   1.314 +  \item Hilbert's $\varepsilon$-operator, 69--71
   1.315 +  \item \isa {hypreal} (type), 137
   1.316  
   1.317    \indexspace
   1.318  
   1.319 @@ -266,9 +265,8 @@
   1.320      \subitem qualified, \bold{2}
   1.321    \item identity function, \bold{94}
   1.322    \item identity relation, \bold{96}
   1.323 -  \item \isa {if} (symbol), \bold{3}, \hyperpage{4}
   1.324 -  \item \isa {iff} (attribute), \hyperpage{73, 74}, \hyperpage{86}, 
   1.325 -		\hyperpage{114}
   1.326 +  \item \isa {if} (symbol), \bold{3}, 4
   1.327 +  \item \isa {iff} (attribute), 73, 74, 86, 114
   1.328    \item \isa {iffD1} (theorem), \bold{78}
   1.329    \item \isa {iffD2} (theorem), \bold{78}
   1.330    \item image
   1.331 @@ -277,292 +275,282 @@
   1.332    \item \isa {image_def} (theorem), \bold{95}
   1.333    \item \isa {Image_iff} (theorem), \bold{96}
   1.334    \item \isa {impI} (theorem), \bold{56}
   1.335 -  \item implication, \hyperpage{56--57}
   1.336 -  \item \isa {induct_tac} (method), \hyperpage{10}, \hyperpage{17}, 
   1.337 -		\hyperpage{50}, \hyperpage{172}
   1.338 -  \item induction, \hyperpage{168--175}
   1.339 -    \subitem recursion, \hyperpage{49--50}
   1.340 +  \item implication, 56--57
   1.341 +  \item \isa {induct_tac} (method), 10, 17, 50, 172
   1.342 +  \item induction, 168--175
   1.343 +    \subitem recursion, 49--50
   1.344      \subitem structural, \bold{17}
   1.345 -    \subitem well-founded, \hyperpage{99}
   1.346 -  \item \isacommand {inductive} (command), \hyperpage{111}
   1.347 +    \subitem well-founded, 99
   1.348 +  \item \isacommand {inductive} (command), 111
   1.349    \item inductive definition
   1.350 -    \subitem simultaneous, \hyperpage{125}
   1.351 -  \item inductive definitions, \hyperpage{111--129}
   1.352 -  \item \isacommand {inductive\_cases} (command), \hyperpage{115}, 
   1.353 -		\hyperpage{123}
   1.354 -  \item \isacommand{infixr} (annotation), \hyperpage{8}
   1.355 +    \subitem simultaneous, 125
   1.356 +  \item inductive definitions, 111--129
   1.357 +  \item \isacommand {inductive\_cases} (command), 115, 123
   1.358 +  \item \isacommand{infixr} (annotation), 8
   1.359    \item \isa {inj_on_def} (theorem), \bold{94}
   1.360 -  \item injections, \hyperpage{94}
   1.361 +  \item injections, 94
   1.362    \item inner syntax, \bold{9}
   1.363 -  \item \isa {insert} (constant), \hyperpage{91}
   1.364 -  \item \isa {insert} (method), \hyperpage{80--82}
   1.365 +  \item \isa {insert} (constant), 91
   1.366 +  \item \isa {insert} (method), 80--82
   1.367    \item instance, \bold{145}
   1.368    \item \texttt {INT}, \bold{189}
   1.369    \item \texttt {Int}, \bold{189}
   1.370 -  \item \isa {int} (type), \hyperpage{135}
   1.371 +  \item \isa {int} (type), 135
   1.372    \item \isa {INT_iff} (theorem), \bold{92}
   1.373    \item \isa {IntD1} (theorem), \bold{89}
   1.374    \item \isa {IntD2} (theorem), \bold{89}
   1.375 -  \item integers, \hyperpage{135}
   1.376 -  \item \isa {INTER} (constant), \hyperpage{93}
   1.377 +  \item integers, 135
   1.378 +  \item \isa {INTER} (constant), 93
   1.379    \item \texttt {Inter}, \bold{189}
   1.380    \item \isa {Inter_iff} (theorem), \bold{92}
   1.381 -  \item intersection, \hyperpage{89}
   1.382 -    \subitem indexed, \hyperpage{92}
   1.383 +  \item intersection, 89
   1.384 +    \subitem indexed, 92
   1.385    \item \isa {IntI} (theorem), \bold{89}
   1.386 -  \item \isa {intro} (method), \hyperpage{58}
   1.387 -  \item \isa {intro!} (attribute), \hyperpage{112}
   1.388 -  \item introduction rules, \hyperpage{52--53}
   1.389 -  \item \isa {inv} (constant), \hyperpage{70}
   1.390 +  \item \isa {intro} (method), 58
   1.391 +  \item \isa {intro!} (attribute), 112
   1.392 +  \item introduction rules, 52--53
   1.393 +  \item \isa {inv} (constant), 70
   1.394    \item \isa {inv_image_def} (theorem), \bold{99}
   1.395    \item inverse
   1.396      \subitem of a function, \bold{94}
   1.397      \subitem of a relation, \bold{96}
   1.398    \item inverse image
   1.399 -    \subitem of a function, \hyperpage{95}
   1.400 -    \subitem of a relation, \hyperpage{98}
   1.401 +    \subitem of a function, 95
   1.402 +    \subitem of a relation, 98
   1.403  
   1.404    \indexspace
   1.405  
   1.406 -  \item \isacommand {kill} (command), \hyperpage{14}
   1.407 +  \item \isacommand {kill} (command), 14
   1.408  
   1.409    \indexspace
   1.410  
   1.411 -  \item \isa {LEAST} (symbol), \hyperpage{21}, \hyperpage{69}
   1.412 +  \item \isa {LEAST} (symbol), 21, 69
   1.413    \item least number operator, \see{\protect\isa{LEAST}}{69}
   1.414 -  \item \isacommand {lemma} (command), \hyperpage{11}
   1.415 -  \item \isacommand {lemmas} (command), \hyperpage{77}, \hyperpage{86}
   1.416 -  \item \isa {length} (symbol), \hyperpage{15}
   1.417 +  \item \isacommand {lemma} (command), 11
   1.418 +  \item \isacommand {lemmas} (command), 77, 86
   1.419 +  \item \isa {length} (symbol), 15
   1.420    \item \isa {length_induct}, \bold{172}
   1.421 -  \item \isa {less_than} (constant), \hyperpage{98}
   1.422 +  \item \isa {less_than} (constant), 98
   1.423    \item \isa {less_than_iff} (theorem), \bold{98}
   1.424 -  \item \isa {let} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{29}
   1.425 +  \item \isa {let} (symbol), \bold{3}, 4, 29
   1.426    \item \isa {lex_prod_def} (theorem), \bold{99}
   1.427 -  \item lexicographic product, \bold{99}, \hyperpage{160}
   1.428 +  \item lexicographic product, \bold{99}, 160
   1.429    \item {\texttt{lfp}}
   1.430      \subitem applications of, \see{CTL}{100}
   1.431 -  \item linear arithmetic, \hyperpage{20--21}, \hyperpage{31}, 
   1.432 -		\hyperpage{131}
   1.433 -  \item \isa {List} (theory), \hyperpage{15}
   1.434 -  \item \isa {list} (type), \hyperpage{2}, \hyperpage{7}, 
   1.435 -		\hyperpage{15}
   1.436 +  \item linear arithmetic, 20--21, 31, 131
   1.437 +  \item \isa {List} (theory), 15
   1.438 +  \item \isa {list} (type), 2, 7, 15
   1.439    \item \isa {lists_mono} (theorem), \bold{121}
   1.440 -  \item Lowe, Gavin, \hyperpage{178--179}
   1.441 +  \item Lowe, Gavin, 178--179
   1.442  
   1.443    \indexspace
   1.444  
   1.445 -  \item \isa {Main} (theory), \hyperpage{2}
   1.446 +  \item \isa {Main} (theory), 2
   1.447    \item major premise, \bold{59}
   1.448 -  \item \isa {max} (constant), \hyperpage{20, 21}
   1.449 +  \item \isa {max} (constant), 20, 21
   1.450    \item measure function, \bold{45}, \bold{98}
   1.451    \item \isa {measure_def} (theorem), \bold{99}
   1.452    \item meta-logic, \bold{64}
   1.453    \item methods, \bold{14}
   1.454 -  \item \isa {min} (constant), \hyperpage{20, 21}
   1.455 -  \item \isa {mod} (symbol), \hyperpage{20}
   1.456 +  \item \isa {min} (constant), 20, 21
   1.457 +  \item \isa {mod} (symbol), 20
   1.458    \item \isa {mod_div_equality} (theorem), \bold{133}
   1.459    \item \isa {mod_mult_distrib} (theorem), \bold{133}
   1.460 -  \item \emph{modus ponens}, \hyperpage{51}, \hyperpage{56}
   1.461 +  \item \emph{modus ponens}, 51, 56
   1.462    \item \isa {mono_def} (theorem), \bold{100}
   1.463 -  \item monotone functions, \bold{100}, \hyperpage{123}
   1.464 -    \subitem and inductive definitions, \hyperpage{121--122}
   1.465 -  \item \isa {more} (constant), \hyperpage{140--142}
   1.466 +  \item monotone functions, \bold{100}, 123
   1.467 +    \subitem and inductive definitions, 121--122
   1.468 +  \item \isa {more} (constant), 140--142
   1.469    \item \isa {mp} (theorem), \bold{56}
   1.470    \item multiset ordering, \bold{99}
   1.471  
   1.472    \indexspace
   1.473  
   1.474 -  \item \isa {nat} (type), \hyperpage{2}, \hyperpage{20}, 
   1.475 -		\hyperpage{133--134}
   1.476 -  \item natural deduction, \hyperpage{51--52}
   1.477 -  \item natural numbers, \hyperpage{133--134}
   1.478 -  \item Needham-Schroeder protocol, \hyperpage{177--179}
   1.479 -  \item negation, \hyperpage{57--59}
   1.480 -  \item \isa {Nil} (constant), \hyperpage{7}
   1.481 +  \item \isa {nat} (type), 2, 20, 133--134
   1.482 +  \item natural deduction, 51--52
   1.483 +  \item natural numbers, 133--134
   1.484 +  \item Needham-Schroeder protocol, 177--179
   1.485 +  \item negation, 57--59
   1.486 +  \item \isa {Nil} (constant), 7
   1.487    \item \isa {no_asm}, \bold{27}
   1.488    \item \isa {no_asm_simp}, \bold{27}
   1.489    \item \isa {no_asm_use}, \bold{28}
   1.490 -  \item non-standard reals, \hyperpage{137}
   1.491 +  \item non-standard reals, 137
   1.492    \item \isa {None} (constant), \bold{22}
   1.493    \item \isa {notE} (theorem), \bold{57}
   1.494    \item \isa {notI} (theorem), \bold{57}
   1.495 -  \item numeric literals, \hyperpage{132}
   1.496 -    \subitem for type \protect\isa{nat}, \hyperpage{133}
   1.497 -    \subitem for type \protect\isa{real}, \hyperpage{136}
   1.498 +  \item numeric literals, 132
   1.499 +    \subitem for type \protect\isa{nat}, 133
   1.500 +    \subitem for type \protect\isa{real}, 136
   1.501  
   1.502    \indexspace
   1.503  
   1.504 -  \item \isa {O} (symbol), \hyperpage{96}
   1.505 +  \item \isa {O} (symbol), 96
   1.506    \item \texttt {o}, \bold{189}
   1.507    \item \isa {o_def} (theorem), \bold{94}
   1.508 -  \item \isa {OF} (attribute), \hyperpage{78--79}
   1.509 -  \item \isa {of} (attribute), \hyperpage{77}, \hyperpage{79}
   1.510 -  \item \isacommand {oops} (command), \hyperpage{11}
   1.511 +  \item \isa {OF} (attribute), 78--79
   1.512 +  \item \isa {of} (attribute), 77, 79
   1.513 +  \item \isacommand {oops} (command), 11
   1.514    \item \isa {option} (type), \bold{22}
   1.515    \item ordered rewriting, \bold{158}
   1.516    \item outer syntax, \bold{9}
   1.517 -  \item overloading, \hyperpage{144--146}
   1.518 -    \subitem and arithmetic, \hyperpage{132}
   1.519 +  \item overloading, 144--146
   1.520 +    \subitem and arithmetic, 132
   1.521  
   1.522    \indexspace
   1.523  
   1.524 -  \item pairs and tuples, \hyperpage{21}, \hyperpage{137--140}
   1.525 +  \item pairs and tuples, 21, 137--140
   1.526    \item parent theory, \bold{2}
   1.527 -  \item partial function, \hyperpage{164}
   1.528 +  \item partial function, 164
   1.529    \item pattern, higher-order, \bold{159}
   1.530 -  \item PDL, \hyperpage{102--105}
   1.531 +  \item PDL, 102--105
   1.532    \item permutative rewrite rule, \bold{158}
   1.533 -  \item \isacommand {pr} (command), \hyperpage{14}, \hyperpage{83}
   1.534 -  \item \isacommand {prefer} (command), \hyperpage{14}, \hyperpage{84}
   1.535 +  \item \isacommand {pr} (command), 14, 83
   1.536 +  \item \isacommand {prefer} (command), 14, 84
   1.537    \item primitive recursion, \see{\isacommand{primrec}}{1}
   1.538 -  \item \isacommand {primrec} (command), \hyperpage{8}, \hyperpage{16}, 
   1.539 -		\hyperpage{36--42}
   1.540 +  \item \isacommand {primrec} (command), 8, 16, 36--42
   1.541    \item product type, \see{pairs and tuples}{1}
   1.542    \item Proof General, \bold{5}
   1.543    \item proofs
   1.544      \subitem abandoning, \bold{11}
   1.545 -    \subitem examples of failing, \hyperpage{71--72}
   1.546 +    \subitem examples of failing, 71--72
   1.547    \item protocols
   1.548 -    \subitem security, \hyperpage{177--187}
   1.549 +    \subitem security, 177--187
   1.550  
   1.551    \indexspace
   1.552  
   1.553    \item quantifiers
   1.554 -    \subitem and inductive definitions, \hyperpage{119--121}
   1.555 -    \subitem existential, \hyperpage{66}
   1.556 -    \subitem for sets, \hyperpage{92}
   1.557 -    \subitem instantiating, \hyperpage{68}
   1.558 -    \subitem universal, \hyperpage{63--66}
   1.559 +    \subitem and inductive definitions, 119--121
   1.560 +    \subitem existential, 66
   1.561 +    \subitem for sets, 92
   1.562 +    \subitem instantiating, 68
   1.563 +    \subitem universal, 63--66
   1.564  
   1.565    \indexspace
   1.566  
   1.567    \item \isa {r_into_rtrancl} (theorem), \bold{96}
   1.568    \item \isa {r_into_trancl} (theorem), \bold{97}
   1.569    \item range
   1.570 -    \subitem of a function, \hyperpage{95}
   1.571 -    \subitem of a relation, \hyperpage{96}
   1.572 -  \item \isa {range} (symbol), \hyperpage{95}
   1.573 +    \subitem of a function, 95
   1.574 +    \subitem of a relation, 96
   1.575 +  \item \isa {range} (symbol), 95
   1.576    \item \isa {Range_iff} (theorem), \bold{96}
   1.577 -  \item \isa {Real} (theory), \hyperpage{137}
   1.578 -  \item \isa {real} (type), \hyperpage{136--137}
   1.579 -  \item real numbers, \hyperpage{136--137}
   1.580 -  \item \isacommand {recdef} (command), \hyperpage{45--50}, 
   1.581 -		\hyperpage{98}, \hyperpage{160--168}
   1.582 -    \subitem and numeric literals, \hyperpage{132}
   1.583 -  \item \isa {recdef_cong} (attribute), \hyperpage{164}
   1.584 -  \item \isa {recdef_simp} (attribute), \hyperpage{47}
   1.585 -  \item \isa {recdef_wf} (attribute), \hyperpage{162}
   1.586 -  \item \isacommand {record} (command), \hyperpage{140}
   1.587 -  \item \isa {record_split} (method), \hyperpage{143}
   1.588 -  \item records, \hyperpage{140--144}
   1.589 -    \subitem extensible, \hyperpage{141--142}
   1.590 +  \item \isa {Real} (theory), 137
   1.591 +  \item \isa {real} (type), 136--137
   1.592 +  \item real numbers, 136--137
   1.593 +  \item \isacommand {recdef} (command), 45--50, 98, 160--168
   1.594 +    \subitem and numeric literals, 132
   1.595 +  \item \isa {recdef_cong} (attribute), 164
   1.596 +  \item \isa {recdef_simp} (attribute), 47
   1.597 +  \item \isa {recdef_wf} (attribute), 162
   1.598 +  \item \isacommand {record} (command), 140
   1.599 +  \item \isa {record_split} (method), 143
   1.600 +  \item records, 140--144
   1.601 +    \subitem extensible, 141--142
   1.602    \item recursion
   1.603      \subitem well-founded, \bold{161}
   1.604 -  \item recursion induction, \hyperpage{49--50}
   1.605 -  \item \isacommand {redo} (command), \hyperpage{14}
   1.606 -  \item reflexive and transitive closure, \hyperpage{96--98}
   1.607 -  \item relations, \hyperpage{95--98}
   1.608 -    \subitem well-founded, \hyperpage{98--99}
   1.609 -  \item \isa {rename_tac} (method), \hyperpage{66--67}
   1.610 -  \item \isa {rev} (constant), \hyperpage{8}
   1.611 +  \item recursion induction, 49--50
   1.612 +  \item \isacommand {redo} (command), 14
   1.613 +  \item reflexive and transitive closure, 96--98
   1.614 +  \item relations, 95--98
   1.615 +    \subitem well-founded, 98--99
   1.616 +  \item \isa {rename_tac} (method), 66--67
   1.617 +  \item \isa {rev} (constant), 8
   1.618    \item rewrite rule, \bold{26}
   1.619      \subitem permutative, \bold{158}
   1.620    \item rewriting, \bold{26}
   1.621      \subitem ordered, \bold{158}
   1.622 -  \item \isa {rotate_tac} (method), \hyperpage{28}
   1.623 +  \item \isa {rotate_tac} (method), 28
   1.624    \item \isa {rtrancl_refl} (theorem), \bold{96}
   1.625    \item \isa {rtrancl_trans} (theorem), \bold{96}
   1.626 -  \item rule induction, \hyperpage{112--114}
   1.627 -  \item rule inversion, \hyperpage{114--115}, \hyperpage{123--124}
   1.628 -  \item \isa {rule_tac} (method), \hyperpage{60}
   1.629 -    \subitem and renaming, \hyperpage{67}
   1.630 +  \item rule induction, 112--114
   1.631 +  \item rule inversion, 114--115, 123--124
   1.632 +  \item \isa {rule_tac} (method), 60
   1.633 +    \subitem and renaming, 67
   1.634  
   1.635    \indexspace
   1.636  
   1.637 -  \item \isa {safe} (method), \hyperpage{75, 76}
   1.638 +  \item \isa {safe} (method), 75, 76
   1.639    \item safe rules, \bold{73}
   1.640 -  \item \isa {set} (type), \hyperpage{2}, \hyperpage{89}
   1.641 -  \item set comprehensions, \hyperpage{91--92}
   1.642 +  \item \isa {set} (type), 2, 89
   1.643 +  \item set comprehensions, 91--92
   1.644    \item \isa {set_ext} (theorem), \bold{90}
   1.645 -  \item sets, \hyperpage{89--93}
   1.646 -    \subitem finite, \hyperpage{93}
   1.647 +  \item sets, 89--93
   1.648 +    \subitem finite, 93
   1.649      \subitem notation for finite, \bold{91}
   1.650    \item settings, \see{flags}{1}
   1.651 -  \item \isa {show_brackets} (flag), \hyperpage{4}
   1.652 -  \item \isa {show_types} (flag), \hyperpage{3}
   1.653 -  \item \texttt {show_types}, \hyperpage{14}
   1.654 -  \item \isa {simp} (attribute), \bold{9}, \hyperpage{26}
   1.655 +  \item \isa {show_brackets} (flag), 4
   1.656 +  \item \isa {show_types} (flag), 3
   1.657 +  \item \texttt {show_types}, 14
   1.658 +  \item \isa {simp} (attribute), \bold{9}, 26
   1.659    \item \isa {simp} (method), \bold{26}
   1.660 -  \item \isa {simp_all} (method), \hyperpage{26}, \hyperpage{36}
   1.661 -  \item simplification, \hyperpage{25--32}, \hyperpage{157--160}
   1.662 -    \subitem of let-expressions, \hyperpage{29}
   1.663 +  \item \isa {simp_all} (method), 26, 36
   1.664 +  \item simplification, 25--32, 157--160
   1.665 +    \subitem of let-expressions, 29
   1.666      \subitem ordered, \bold{158}
   1.667 -    \subitem with definitions, \hyperpage{28}
   1.668 -    \subitem with/of assumptions, \hyperpage{27}
   1.669 -  \item simplification rule, \bold{26}, \hyperpage{159--160}
   1.670 -  \item \isa {simplified} (attribute), \hyperpage{77}, \hyperpage{79}
   1.671 +    \subitem with definitions, 28
   1.672 +    \subitem with/of assumptions, 27
   1.673 +  \item simplification rule, \bold{26}, 159--160
   1.674 +  \item \isa {simplified} (attribute), 77, 79
   1.675    \item simplifier, \bold{25}
   1.676 -  \item \isa {size} (constant), \hyperpage{15}
   1.677 -  \item \isa {snd} (constant), \hyperpage{21}
   1.678 -  \item \isa {SOME} (symbol), \hyperpage{69}
   1.679 +  \item \isa {size} (constant), 15
   1.680 +  \item \isa {snd} (constant), 21
   1.681 +  \item \isa {SOME} (symbol), 69
   1.682    \item \texttt {SOME}, \bold{189}
   1.683    \item \isa {Some} (constant), \bold{22}
   1.684    \item \isa {some_equality} (theorem), \bold{69}
   1.685    \item \isa {someI} (theorem), \bold{70}
   1.686    \item \isa {someI2} (theorem), \bold{70}
   1.687    \item \isa {someI_ex} (theorem), \bold{71}
   1.688 -  \item sorts, \hyperpage{150}
   1.689 +  \item sorts, 150
   1.690    \item \isa {spec} (theorem), \bold{64}
   1.691    \item \isa {split} (constant), \bold{137}
   1.692 -  \item \isa {split} (method, attr.), \hyperpage{29--31}
   1.693 +  \item \isa {split} (method, attr.), 29--31
   1.694    \item split rule, \bold{30}
   1.695 -  \item \isa {split_if} (theorem), \hyperpage{30}
   1.696 +  \item \isa {split_if} (theorem), 30
   1.697    \item \isa {ssubst} (theorem), \bold{61}
   1.698    \item structural induction, \bold{17}
   1.699 -  \item \isa {subgoal_tac} (method), \hyperpage{81, 82}
   1.700 +  \item \isa {subgoal_tac} (method), 81, 82
   1.701    \item subset relation, \bold{90}
   1.702    \item \isa {subsetD} (theorem), \bold{90}
   1.703    \item \isa {subsetI} (theorem), \bold{90}
   1.704 -  \item \isa {subst} (method), \hyperpage{61}
   1.705 -  \item substitution, \hyperpage{61--63}
   1.706 -  \item \isa {Suc} (constant), \hyperpage{20}
   1.707 +  \item \isa {subst} (method), 61
   1.708 +  \item substitution, 61--63
   1.709 +  \item \isa {Suc} (constant), 20
   1.710    \item \isa {surj_def} (theorem), \bold{94}
   1.711 -  \item surjections, \hyperpage{94}
   1.712 +  \item surjections, 94
   1.713    \item \isa {sym} (theorem), \bold{77}
   1.714 -  \item syntax translations, \hyperpage{23--24}
   1.715  
   1.716    \indexspace
   1.717  
   1.718 -  \item tacticals, \hyperpage{82--83}
   1.719 -  \item tactics, \hyperpage{10}
   1.720 -  \item \isacommand {term} (command), \hyperpage{14}
   1.721 +  \item tacticals, 82--83
   1.722 +  \item tactics, 10
   1.723 +  \item \isacommand {term} (command), 14
   1.724    \item term rewriting, \bold{26}
   1.725    \item termination, \see{functions, total}{1}
   1.726 -  \item terms, \hyperpage{3}
   1.727 -  \item \isa {THEN} (attribute), \bold{77}, \hyperpage{79}, 
   1.728 -		\hyperpage{86}
   1.729 -  \item \isacommand {theorem} (command), \bold{9}, \hyperpage{11}
   1.730 -  \item theories, \hyperpage{2}
   1.731 +  \item terms, 3
   1.732 +  \item \isa {THEN} (attribute), \bold{77}, 79, 86
   1.733 +  \item \isacommand {theorem} (command), \bold{9}, 11
   1.734 +  \item theories, 2
   1.735      \subitem abandoning, \bold{14}
   1.736 -  \item theory files, \hyperpage{2}
   1.737 -  \item \isacommand {thm} (command), \hyperpage{14}
   1.738 -  \item \isa {tl} (constant), \hyperpage{15}
   1.739 -  \item \isa {trace_simp} (flag), \hyperpage{31}
   1.740 +  \item theory files, 2
   1.741 +  \item \isacommand {thm} (command), 14
   1.742 +  \item \isa {tl} (constant), 15
   1.743 +  \item \isa {trace_simp} (flag), 31
   1.744    \item tracing the simplifier, \bold{31}
   1.745    \item \isa {trancl_trans} (theorem), \bold{97}
   1.746 -  \item \isa {True} (constant), \hyperpage{3}
   1.747 +  \item \isa {True} (constant), 3
   1.748    \item tuples, \see{pairs and tuples}{1}
   1.749 -  \item \isacommand {typ} (command), \hyperpage{14}
   1.750 +  \item \isacommand {typ} (command), 14
   1.751    \item type constraints, \bold{4}
   1.752    \item type inference, \bold{3}
   1.753 -  \item type synonyms, \hyperpage{22--23}
   1.754    \item type variables, \bold{3}
   1.755 -  \item \isacommand {typedecl} (command), \hyperpage{150}
   1.756 -  \item \isacommand {typedef} (command), \hyperpage{151--155}
   1.757 -  \item types, \hyperpage{2}
   1.758 -    \subitem declaring, \hyperpage{150--151}
   1.759 -    \subitem defining, \hyperpage{151--155}
   1.760 -  \item \isacommand {types} (command), \hyperpage{22}
   1.761 +  \item \isacommand {typedecl} (command), 150
   1.762 +  \item \isacommand {typedef} (command), 151--155
   1.763 +  \item types, 2
   1.764 +    \subitem declaring, 150--151
   1.765 +    \subitem defining, 151--155
   1.766 +  \item \isacommand {types} (command), 22
   1.767  
   1.768    \indexspace
   1.769  
   1.770 @@ -572,15 +560,15 @@
   1.771    \item \isa {UN_I} (theorem), \bold{92}
   1.772    \item \isa {UN_iff} (theorem), \bold{92}
   1.773    \item \isa {Un_subset_iff} (theorem), \bold{90}
   1.774 -  \item \isacommand {undo} (command), \hyperpage{14}
   1.775 -  \item unification, \hyperpage{60--63}
   1.776 -  \item \isa {UNION} (constant), \hyperpage{93}
   1.777 +  \item \isacommand {undo} (command), 14
   1.778 +  \item unification, 60--63
   1.779 +  \item \isa {UNION} (constant), 93
   1.780    \item \texttt {Union}, \bold{189}
   1.781    \item union
   1.782 -    \subitem indexed, \hyperpage{92}
   1.783 +    \subitem indexed, 92
   1.784    \item \isa {Union_iff} (theorem), \bold{92}
   1.785 -  \item \isa {unit} (type), \hyperpage{22}
   1.786 -  \item unknowns, \hyperpage{4}, \bold{52}
   1.787 +  \item \isa {unit} (type), 22
   1.788 +  \item unknowns, 4, \bold{52}
   1.789    \item unsafe rules, \bold{73}
   1.790    \item updating a function, \bold{93}
   1.791  
   1.792 @@ -588,14 +576,14 @@
   1.793  
   1.794    \item variable, \bold{4}
   1.795    \item variables
   1.796 -    \subitem schematic, \hyperpage{4}
   1.797 +    \subitem schematic, 4
   1.798      \subitem type, \bold{3}
   1.799    \item \isa {vimage_def} (theorem), \bold{95}
   1.800  
   1.801    \indexspace
   1.802  
   1.803    \item \isa {wf_induct} (theorem), \bold{99}
   1.804 -  \item \isa {while} (constant), \hyperpage{167}
   1.805 -  \item \isa {While_Combinator} (theory), \hyperpage{167}
   1.806 +  \item \isa {while} (constant), 167
   1.807 +  \item \isa {While_Combinator} (theory), 167
   1.808  
   1.809  \end{theindex}