working
authorpaulson
Fri Jul 13 18:28:46 2001 +0200 (2001-07-13)
changeset 11424aa0571fb96b9
parent 11423 49312d90cf1f
child 11425 4988fd27d6e6
working
doc-src/TutorialI/tutorial.ind
     1.1 --- a/doc-src/TutorialI/tutorial.ind	Fri Jul 13 18:22:13 2001 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.ind	Fri Jul 13 18:28:46 2001 +0200
     1.3 @@ -1,25 +1,28 @@
     1.4  \begin{theindex}
     1.5  
     1.6 -  \item \emph {$\forall \tmspace +\thinmuskip {.1667em}$}, \bold{3}, 
     1.7 -		\bold{189}
     1.8 +  \item \emph {$\forall \tmspace +\thinmuskip {.1667em}$}, \bold{189}
     1.9 +  \item \isasymforall, \bold{3}
    1.10    \item \ttall, \bold{189}
    1.11 -  \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{3}, 
    1.12 -		\bold{189}
    1.13 +  \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{189}
    1.14 +  \item \isasymexists, \bold{3}
    1.15    \item \texttt{?}, \hyperpage{5}, \bold{189}
    1.16    \item \emph {$\varepsilon $}, \bold{189}
    1.17    \item \isasymuniqex, \bold{3}, \bold{189}
    1.18    \item \ttuniquex, \bold{189}
    1.19 -  \item \emph {$\wedge $}, \bold{3}, \bold{189}
    1.20 +  \item \emph {$\wedge $}, \bold{189}
    1.21 +  \item \isasymand, \bold{3}
    1.22    \item {\texttt {\&}}, \bold{189}
    1.23    \item \texttt {=}, \bold{3}
    1.24 -  \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{3}, 
    1.25 -		\bold{189}
    1.26 +  \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{189}
    1.27 +  \item \isasymimp, \bold{3}
    1.28    \item \texttt {-->}, \bold{189}
    1.29 -  \item \emph {$\neg $}, \bold{3}, \bold{189}
    1.30 +  \item \emph {$\neg $}, \bold{189}
    1.31 +  \item \isasymnot, \bold{3}
    1.32    \item \verb$~$, \bold{189}
    1.33    \item \emph {$\not =$}, \bold{189}
    1.34    \item \verb$~=$, \bold{189}
    1.35 -  \item \emph {$\vee $}, \bold{3}, \bold{189}
    1.36 +  \item \emph {$\vee $}, \bold{189}
    1.37 +  \item \isasymor, \bold{3}
    1.38    \item \ttor, \bold{189}
    1.39    \item \emph {$\circ $}, \bold{189}
    1.40    \item \emph {$\mid $}\nobreakspace {}\emph {$\mid $}, \bold{189}
    1.41 @@ -50,9 +53,9 @@
    1.42    \item \ttAnd, \bold{189}
    1.43    \item \emph {$\equiv $}, \bold{23}, \bold{189}
    1.44    \item \texttt {==}, \bold{189}
    1.45 -  \item \emph {$\rightleftharpoons $}, \bold{23}, \bold{189}
    1.46 -  \item \emph {$\rightharpoonup $}, \bold{23}, \bold{189}
    1.47 -  \item \emph {$\leftharpoondown $}, \bold{23}, \bold{189}
    1.48 +  \item \emph {$\rightleftharpoons $}, \bold{24}, \bold{189}
    1.49 +  \item \emph {$\rightharpoonup $}, \bold{24}, \bold{189}
    1.50 +  \item \emph {$\leftharpoondown $}, \bold{24}, \bold{189}
    1.51    \item \emph {$\Rightarrow $}, \bold{3}, \bold{189}
    1.52    \item \texttt {=>}, \bold{189}
    1.53    \item \texttt {<=}, \bold{189}
    1.54 @@ -77,33 +80,27 @@
    1.55  
    1.56    \indexspace
    1.57  
    1.58 -  \item \isa {0}, \bold{20}
    1.59 -  \item \texttt {0}, \bold{21}
    1.60 +  \item \isa {0} (constant), \hyperpage{20, 21}, \hyperpage{133}
    1.61 +  \item \isa {1} (symbol), \hyperpage{133}
    1.62 +  \item \isa {2} (symbol), \hyperpage{133}
    1.63  
    1.64    \indexspace
    1.65  
    1.66    \item abandon proof, \bold{11}
    1.67    \item abandon theory, \bold{14}
    1.68 +  \item \isa {abs} (constant), \hyperpage{135}
    1.69    \item \texttt {abs}, \bold{189}
    1.70 -  \item \isa {abs_mult} (theorem), \bold{135}
    1.71 -  \item \isa {add_2_eq_Suc} (theorem), \bold{133}
    1.72 -  \item \isa {add_2_eq_Suc'} (theorem), \bold{133}
    1.73 +  \item absolute value, \hyperpage{135}
    1.74    \item \isa {add_assoc} (theorem), \bold{134}
    1.75    \item \isa {add_commute} (theorem), \bold{134}
    1.76 -  \item \isa {add_left_commute} (theorem), \bold{134}
    1.77    \item \isa {add_mult_distrib} (theorem), \bold{133}
    1.78    \item \texttt {ALL}, \bold{189}
    1.79    \item \isa {All} (constant), \hyperpage{93}
    1.80    \item \isa {allE} (theorem), \bold{65}
    1.81    \item \isa {allI} (theorem), \bold{64}
    1.82 -  \item \isa {analz_Crypt_if} (theorem), \bold{186}
    1.83 -  \item \isa {analz_idem} (theorem), \bold{180}
    1.84 -  \item \isa {analz_mono} (theorem), \bold{180}
    1.85 -  \item \isa {analz_synth} (theorem), \bold{180}
    1.86 -  \item \isa {append_take_drop_id} (theorem), \bold{127}
    1.87 -  \item apply, \bold{13}
    1.88 +  \item \isacommand {apply} (command), \hyperpage{13}
    1.89    \item \isa {arg_cong} (theorem), \bold{80}
    1.90 -  \item \isa {arith}, \bold{21}
    1.91 +  \item \isa {arith} (method), \hyperpage{21}, \hyperpage{131}
    1.92    \item arithmetic, \hyperpage{20--21}, \hyperpage{31}
    1.93    \item \textsc {ascii} symbols, \bold{189}
    1.94    \item associative-commutative function, \hyperpage{158}
    1.95 @@ -152,15 +149,10 @@
    1.96    \item \isa {classical} (theorem), \bold{57}
    1.97    \item closure
    1.98      \subitem reflexive and transitive, \hyperpage{96--98}
    1.99 -  \item \isa {coinduct} (theorem), \bold{100}
   1.100    \item coinduction, \bold{100}
   1.101    \item \isa {Collect} (constant), \hyperpage{93}
   1.102 -  \item \isa {Collect_mem_eq} (theorem), \bold{91}
   1.103    \item \isa {comp_def} (theorem), \bold{96}
   1.104 -  \item \isa {comp_mono} (theorem), \bold{96}
   1.105    \item \isa {Compl_iff} (theorem), \bold{90}
   1.106 -  \item \isa {Compl_partition} (theorem), \bold{90}
   1.107 -  \item \isa {Compl_Un} (theorem), \bold{90}
   1.108    \item complement
   1.109      \subitem of a set, \hyperpage{89}
   1.110    \item composition
   1.111 @@ -171,22 +163,16 @@
   1.112    \item \isa {conjI} (theorem), \bold{52}
   1.113    \item \isa {Cons}, \bold{7}
   1.114    \item \isa {constdefs}, \bold{23}
   1.115 -  \item \isa {contrapos_nn} (theorem), \bold{57}
   1.116 -  \item \isa {contrapos_np} (theorem), \bold{57}
   1.117 -  \item \isa {contrapos_pn} (theorem), \bold{57}
   1.118 -  \item \isa {contrapos_pp} (theorem), \bold{57}
   1.119    \item contrapositives, \hyperpage{57}
   1.120    \item converse
   1.121      \subitem of a relation, \bold{96}
   1.122 -  \item \isa {converse_comp} (theorem), \bold{96}
   1.123    \item \isa {converse_iff} (theorem), \bold{96}
   1.124    \item CTL, \hyperpage{100--110}
   1.125  
   1.126    \indexspace
   1.127  
   1.128    \item \isa {datatype}, \hyperpage{7}, \hyperpage{36--42}
   1.129 -  \item \isa {defer}, \bold{14}
   1.130 -  \item \isacommand {defer} (command), \hyperpage{84}
   1.131 +  \item \isacommand {defer} (command), \hyperpage{14}, \hyperpage{84}
   1.132    \item definition, \bold{23}
   1.133      \subitem unfolding, \bold{28}
   1.134    \item \isa {defs}, \bold{23}
   1.135 @@ -195,32 +181,26 @@
   1.136      \subitem indefinite, \hyperpage{70}
   1.137    \item \isa {dest} (attribute), \hyperpage{86}
   1.138    \item destruction rules, \hyperpage{55}
   1.139 -  \item \isa {Diff_disjoint} (theorem), \bold{90}
   1.140    \item \isa {diff_mult_distrib} (theorem), \bold{133}
   1.141    \item difference
   1.142      \subitem of sets, \bold{90}
   1.143    \item \isa {disjCI} (theorem), \bold{58}
   1.144    \item \isa {disjE} (theorem), \bold{54}
   1.145    \item \isa {div}, \bold{20}
   1.146 -  \item \isa {div_le_mono} (theorem), \bold{133}
   1.147 -  \item \isa {div_mult1_eq} (theorem), \bold{133}
   1.148 -  \item \isa {div_mult2_eq} (theorem), \bold{133}
   1.149 -  \item \isa {div_mult_mult1} (theorem), \bold{133}
   1.150 -  \item divides relation, \bold{68}, \hyperpage{78}, \hyperpage{85--87}
   1.151 -  \item \isa {DIVISION_BY_ZERO_DIV} (theorem), \bold{134}
   1.152 -  \item \isa {DIVISION_BY_ZERO_MOD} (theorem), \bold{134}
   1.153 +  \item divides relation, \hyperpage{68}, \hyperpage{78}, 
   1.154 +		\hyperpage{85--87}, \hyperpage{134}
   1.155 +  \item division
   1.156 +    \subitem by negative numbers, \hyperpage{135}
   1.157 +    \subitem by zero, \hyperpage{134}
   1.158 +    \subitem for type \protect\isa{nat}, \hyperpage{133}
   1.159    \item domain
   1.160      \subitem of a relation, \hyperpage{96}
   1.161    \item \isa {Domain_iff} (theorem), \bold{96}
   1.162    \item done, \bold{11}
   1.163    \item \isa {drule_tac} (method), \hyperpage{60}, \hyperpage{80}
   1.164 -  \item \isa {dvd_add} (theorem), \bold{79}, \bold{134}
   1.165 +  \item \isa {dvd_add} (theorem), \bold{134}
   1.166    \item \isa {dvd_anti_sym} (theorem), \bold{134}
   1.167 -  \item \isa {dvd_def} (theorem), \bold{68}, \bold{78}, \bold{134}
   1.168 -  \item \isa {dvd_mod} (theorem), \bold{87}
   1.169 -  \item \isa {dvd_mod_imp_dvd} (theorem), \bold{86}
   1.170 -  \item \isa {dvd_refl} (theorem), \bold{79}
   1.171 -  \item \isa {dvd_trans} (theorem), \bold{87}
   1.172 +  \item \isa {dvd_def} (theorem), \bold{134}
   1.173  
   1.174    \indexspace
   1.175  
   1.176 @@ -237,15 +217,10 @@
   1.177    \item Euclid's algorithm, \hyperpage{85--87}
   1.178    \item even numbers
   1.179      \subitem defining inductively, \hyperpage{111--115}
   1.180 -  \item \isa {even.cases} (theorem), \bold{114}
   1.181 -  \item \isa {even.induct} (theorem), \bold{112}
   1.182 -  \item \isa {even.step} (theorem), \bold{112}
   1.183 -  \item \isa {even.zero} (theorem), \bold{112}
   1.184    \item \texttt {EX}, \bold{189}
   1.185    \item \isa {Ex} (constant), \hyperpage{93}
   1.186    \item \isa {exE} (theorem), \bold{66}
   1.187    \item \isa {exI} (theorem), \bold{66}
   1.188 -  \item \isa {expand_fun_eq} (theorem), \bold{94}
   1.189    \item \isa {ext} (theorem), \bold{93}
   1.190    \item extensionality
   1.191      \subitem for functions, \bold{93, 94}
   1.192 @@ -267,25 +242,21 @@
   1.193    \item \isa {frule} (method), \hyperpage{67}
   1.194    \item \isa {frule_tac} (method), \hyperpage{60}
   1.195    \item \isa {fst}, \bold{21}
   1.196 -  \item \isa {fun_upd_apply} (theorem), \bold{94}
   1.197 -  \item \isa {fun_upd_upd} (theorem), \bold{94}
   1.198    \item functions, \hyperpage{93--95}
   1.199  
   1.200    \indexspace
   1.201  
   1.202    \item \isa {gcd} (constant), \hyperpage{76--78}, \hyperpage{85--87}
   1.203 -  \item \isa {gcd_mult_distrib2} (theorem), \bold{77}
   1.204    \item generalizing for induction, \hyperpage{113}
   1.205 -  \item \isa {gfp_unfold} (theorem), \bold{100}
   1.206    \item Girard, Jean-Yves, \fnote{55}
   1.207    \item ground terms example, \hyperpage{119--124}
   1.208 -  \item \isa {gterm_Apply_elim} (theorem), \bold{123}
   1.209  
   1.210    \indexspace
   1.211  
   1.212 -  \item \isa {hd}, \bold{15}
   1.213 +  \item \isa {hd} (constant), \hyperpage{15}
   1.214    \item higher-order pattern, \bold{159}
   1.215    \item Hilbert's $\varepsilon$-operator, \hyperpage{69--71}
   1.216 +  \item {\textit {hypreal}} (type), \hyperpage{137}
   1.217  
   1.218    \indexspace
   1.219  
   1.220 @@ -303,11 +274,8 @@
   1.221    \item image
   1.222      \subitem under a function, \bold{95}
   1.223      \subitem under a relation, \bold{96}
   1.224 -  \item \isa {image_compose} (theorem), \bold{95}
   1.225    \item \isa {image_def} (theorem), \bold{95}
   1.226    \item \isa {Image_iff} (theorem), \bold{96}
   1.227 -  \item \isa {image_Int} (theorem), \bold{95}
   1.228 -  \item \isa {image_Un} (theorem), \bold{95}
   1.229    \item \isa {impI} (theorem), \bold{56}
   1.230    \item implication, \hyperpage{56--57}
   1.231    \item \isa {induct_tac}, \hyperpage{10}, \hyperpage{17}, 
   1.232 @@ -327,13 +295,14 @@
   1.233    \item inner syntax, \bold{9}
   1.234    \item \isa {insert} (constant), \hyperpage{91}
   1.235    \item \isa {insert} (method), \hyperpage{80--82}
   1.236 -  \item \isa {insert_is_Un} (theorem), \bold{91}
   1.237    \item instance, \bold{145}
   1.238    \item \texttt {INT}, \bold{189}
   1.239    \item \texttt {Int}, \bold{189}
   1.240 +  \item \isa {int} (type), \hyperpage{135}
   1.241    \item \isa {INT_iff} (theorem), \bold{92}
   1.242    \item \isa {IntD1} (theorem), \bold{89}
   1.243    \item \isa {IntD2} (theorem), \bold{89}
   1.244 +  \item integers, \hyperpage{135}
   1.245    \item \isa {INTER} (constant), \hyperpage{93}
   1.246    \item \texttt {Inter}, \bold{189}
   1.247    \item \isa {Inter_iff} (theorem), \bold{92}
   1.248 @@ -344,10 +313,7 @@
   1.249    \item \isa {intro!} (attribute), \hyperpage{112}
   1.250    \item introduction rules, \hyperpage{52--53}
   1.251    \item \isa {inv} (constant), \hyperpage{70}
   1.252 -  \item \isa {inv_def} (theorem), \bold{70}
   1.253 -  \item \isa {inv_f_f} (theorem), \bold{94}
   1.254    \item \isa {inv_image_def} (theorem), \bold{99}
   1.255 -  \item \isa {inv_inv_eq} (theorem), \bold{94}
   1.256    \item inverse
   1.257      \subitem of a function, \bold{94}
   1.258      \subitem of a relation, \bold{96}
   1.259 @@ -357,17 +323,16 @@
   1.260  
   1.261    \indexspace
   1.262  
   1.263 -  \item \isa {kill}, \bold{14}
   1.264 +  \item \isacommand {kill} (command), \hyperpage{14}
   1.265  
   1.266    \indexspace
   1.267  
   1.268 -  \item \isa {le_less_trans} (theorem), \bold{171}
   1.269 -  \item \isa {LEAST}, \bold{20}
   1.270 +  \item \isa {LEAST}, \bold{21}
   1.271    \item least number operator, \hyperpage{69}
   1.272    \item lemma, \hyperpage{11}
   1.273    \item \isa {lemma}, \bold{11}
   1.274    \item \isacommand {lemmas} (command), \hyperpage{77}, \hyperpage{86}
   1.275 -  \item \isa {length}, \bold{15}
   1.276 +  \item \isa {length} (symbol), \hyperpage{15}
   1.277    \item \isa {length_induct}, \bold{172}
   1.278    \item \isa {less_than} (constant), \hyperpage{98}
   1.279    \item \isa {less_than_iff} (theorem), \bold{98}
   1.280 @@ -376,11 +341,8 @@
   1.281    \item lexicographic product, \bold{99}, \hyperpage{160}
   1.282    \item {\texttt{lfp}}
   1.283      \subitem applications of, \see{CTL}{100}
   1.284 -  \item \isa {lfp_induct} (theorem), \bold{100}
   1.285 -  \item \isa {lfp_unfold} (theorem), \bold{100}
   1.286 -  \item linear arithmetic, \bold{21}
   1.287 +  \item linear arithmetic, \bold{21}, \hyperpage{131}
   1.288    \item \isa {list}, \hyperpage{2}, \bold{7}, \bold{15}
   1.289 -  \item \isa {lists_Int_eq} (theorem), \bold{123}
   1.290    \item \isa {lists_mono} (theorem), \bold{121}
   1.291  
   1.292    \indexspace
   1.293 @@ -390,64 +352,52 @@
   1.294    \item \isa {max}, \bold{20, 21}
   1.295    \item measure function, \bold{45}, \bold{98}
   1.296    \item \isa {measure_def} (theorem), \bold{99}
   1.297 -  \item \isa {mem_Collect_eq} (theorem), \bold{91}
   1.298    \item meta-logic, \bold{64}
   1.299 -  \item method, \bold{14}
   1.300 +  \item methods, \bold{14}
   1.301    \item \isa {min}, \bold{20, 21}
   1.302    \item \isa {mod}, \bold{20}
   1.303 -  \item \isa {mod_div_equality} (theorem), \bold{81}, \bold{133}
   1.304 -  \item \isa {mod_if} (theorem), \bold{133}
   1.305 -  \item \isa {mod_mult1_eq} (theorem), \bold{133}
   1.306 -  \item \isa {mod_mult2_eq} (theorem), \bold{133}
   1.307 +  \item \isa {mod_div_equality} (theorem), \bold{133}
   1.308    \item \isa {mod_mult_distrib} (theorem), \bold{133}
   1.309 -  \item \isa {mod_Suc} (theorem), \bold{80}
   1.310    \item \emph{modus ponens}, \hyperpage{51}, \hyperpage{56}
   1.311    \item \isa {mono_def} (theorem), \bold{100}
   1.312 -  \item \isa {mono_Int} (theorem), \bold{123}
   1.313 -  \item \isa {monoD} (theorem), \bold{100}
   1.314 -  \item \isa {monoI} (theorem), \bold{100}
   1.315    \item monotone functions, \bold{100}, \hyperpage{123}
   1.316      \subitem and inductive definitions, \hyperpage{121--122}
   1.317    \item \isa {mp} (theorem), \bold{56}
   1.318 -  \item \isa {mult_commute} (theorem), \bold{61}
   1.319 -  \item \isa {mult_le_mono} (theorem), \bold{133}
   1.320 -  \item \isa {mult_le_mono1} (theorem), \bold{80}
   1.321 -  \item \isa {mult_less_mono1} (theorem), \bold{133}
   1.322    \item multiset ordering, \bold{99}
   1.323  
   1.324    \indexspace
   1.325  
   1.326 -  \item \isa {n_subsets} (theorem), \bold{93}
   1.327 -  \item \isa {nat}, \hyperpage{2}, \bold{20}
   1.328 -  \item \isa {nat_diff_split} (theorem), \bold{134}
   1.329 +  \item \isa {nat}, \hyperpage{2}
   1.330 +  \item \isa {nat} (type), \hyperpage{133--134}
   1.331 +  \item {\textit {nat}} (type), \hyperpage{20}
   1.332    \item natural deduction, \hyperpage{51--52}
   1.333 -  \item \isa {neg_mod_bound} (theorem), \bold{135}
   1.334 -  \item \isa {neg_mod_sign} (theorem), \bold{135}
   1.335 +  \item natural numbers, \hyperpage{133--134}
   1.336    \item negation, \hyperpage{57--59}
   1.337    \item \isa {Nil}, \bold{7}
   1.338    \item \isa {no_asm}, \bold{27}
   1.339    \item \isa {no_asm_simp}, \bold{27}
   1.340    \item \isa {no_asm_use}, \bold{28}
   1.341 +  \item non-standard reals, \hyperpage{137}
   1.342    \item \isa {None}, \bold{22}
   1.343    \item \isa {notE} (theorem), \bold{57}
   1.344    \item \isa {notI} (theorem), \bold{57}
   1.345 -  \item \isa {numeral_0_eq_0} (theorem), \bold{133}
   1.346 -  \item \isa {numeral_1_eq_1} (theorem), \bold{133}
   1.347 +  \item numeric literals, \hyperpage{132}
   1.348 +    \subitem for type \protect\isa{nat}, \hyperpage{133}
   1.349 +    \subitem for type \protect\isa{real}, \hyperpage{136}
   1.350  
   1.351    \indexspace
   1.352  
   1.353    \item \isa {O} (symbol), \hyperpage{96}
   1.354    \item \texttt {o}, \bold{189}
   1.355 -  \item \isa {o_assoc} (theorem), \bold{94}
   1.356    \item \isa {o_def} (theorem), \bold{94}
   1.357    \item \isa {OF} (attribute), \hyperpage{78--79}
   1.358    \item \isa {of} (attribute), \hyperpage{77}, \hyperpage{79}
   1.359    \item \isa {oops}, \bold{11}
   1.360    \item \isa {option}, \bold{22}
   1.361 -  \item \isa {order_antisym} (theorem), \bold{69}
   1.362    \item ordered rewriting, \bold{158}
   1.363    \item outer syntax, \bold{9}
   1.364    \item overloading, \hyperpage{144--146}
   1.365 +    \subitem and arithmetic, \hyperpage{132}
   1.366  
   1.367    \indexspace
   1.368  
   1.369 @@ -457,12 +407,8 @@
   1.370    \item pattern, higher-order, \bold{159}
   1.371    \item PDL, \hyperpage{102--105}
   1.372    \item permutative rewrite rule, \bold{158}
   1.373 -  \item \isa {pos_mod_bound} (theorem), \bold{135}
   1.374 -  \item \isa {pos_mod_sign} (theorem), \bold{135}
   1.375 -  \item \isa {pr}, \bold{14}
   1.376 -  \item \isacommand {pr} (command), \hyperpage{83}
   1.377 -  \item \isa {prefer}, \bold{14}
   1.378 -  \item \isacommand {prefer} (command), \hyperpage{84}
   1.379 +  \item \isacommand {pr} (command), \hyperpage{14}, \hyperpage{83}
   1.380 +  \item \isacommand {prefer} (command), \hyperpage{14}, \hyperpage{84}
   1.381    \item primitive recursion, \bold{16}
   1.382    \item \isa {primrec}, \hyperpage{8}, \bold{16}, \hyperpage{36--42}
   1.383    \item product type, \see{pair}{1}
   1.384 @@ -485,33 +431,26 @@
   1.385  
   1.386    \item \isa {r_into_rtrancl} (theorem), \bold{96}
   1.387    \item \isa {r_into_trancl} (theorem), \bold{97}
   1.388 -  \item \isa {R_O_Id} (theorem), \bold{96}
   1.389    \item range
   1.390      \subitem of a function, \hyperpage{95}
   1.391      \subitem of a relation, \hyperpage{96}
   1.392    \item \isa {range} (symbol), \hyperpage{95}
   1.393    \item \isa {Range_iff} (theorem), \bold{96}
   1.394 -  \item \isa {real_add_divide_distrib} (theorem), \bold{136}
   1.395 -  \item \isa {real_dense} (theorem), \bold{136}
   1.396 -  \item \isa {real_divide_divide1_eq} (theorem), \bold{136}
   1.397 -  \item \isa {real_divide_divide2_eq} (theorem), \bold{136}
   1.398 -  \item \isa {real_divide_minus_eq} (theorem), \bold{136}
   1.399 -  \item \isa {real_minus_divide_eq} (theorem), \bold{136}
   1.400 -  \item \isa {real_times_divide1_eq} (theorem), \bold{136}
   1.401 -  \item \isa {real_times_divide2_eq} (theorem), \bold{136}
   1.402 -  \item \isa {realpow_abs} (theorem), \bold{136}
   1.403 +  \item \isa {real} (type), \hyperpage{136--137}
   1.404 +  \item real numbers, \hyperpage{136--137}
   1.405    \item \isa {recdef}, \hyperpage{45--50}, \hyperpage{160--168}
   1.406    \item \isacommand {recdef} (command), \hyperpage{98}
   1.407 +  \item \protect\isacommand{recdef} (command)
   1.408 +    \subitem and numeric literals, \hyperpage{132}
   1.409    \item \isa {recdef_cong}, \bold{164}
   1.410    \item \isa {recdef_simp}, \bold{47}
   1.411    \item \isa {recdef_wf}, \bold{162}
   1.412    \item recursion
   1.413      \subitem well-founded, \bold{161}
   1.414    \item recursion induction, \hyperpage{49--50}
   1.415 -  \item \isa {redo}, \bold{14}
   1.416 +  \item \isacommand {redo} (command), \hyperpage{14}
   1.417    \item relations, \hyperpage{95--98}
   1.418      \subitem well-founded, \hyperpage{98--99}
   1.419 -  \item \isa {relprime_dvd_mult} (theorem), \bold{78}
   1.420    \item \isa {rename_tac} (method), \hyperpage{66--67}
   1.421    \item \isa {rev}, \bold{8}
   1.422    \item rewrite rule, \bold{26}
   1.423 @@ -519,11 +458,8 @@
   1.424    \item rewriting, \bold{26}
   1.425      \subitem ordered, \bold{158}
   1.426    \item \isa {rotate_tac}, \bold{28}
   1.427 -  \item \isa {rtrancl_idemp} (theorem), \bold{97}
   1.428 -  \item \isa {rtrancl_induct} (theorem), \bold{97}
   1.429    \item \isa {rtrancl_refl} (theorem), \bold{96}
   1.430    \item \isa {rtrancl_trans} (theorem), \bold{96}
   1.431 -  \item \isa {rtrancl_unfold} (theorem), \bold{96}
   1.432    \item rule induction, \hyperpage{112--114}
   1.433    \item rule inversion, \hyperpage{114--115}, \hyperpage{123--124}
   1.434    \item \isa {rule_tac} (method), \hyperpage{60}
   1.435 @@ -555,15 +491,15 @@
   1.436    \item simplification rule, \bold{26}, \hyperpage{159--160}
   1.437    \item \isa {simplified} (attribute), \hyperpage{77}, \hyperpage{79}
   1.438    \item simplifier, \bold{25}
   1.439 -  \item \isa {size}, \bold{15}
   1.440 +  \item \isa {size} (constant), \hyperpage{15}
   1.441    \item \isa {snd}, \bold{21}
   1.442    \item \isa {SOME} (symbol), \hyperpage{69}
   1.443    \item \texttt {SOME}, \bold{189}
   1.444    \item \isa {Some}, \bold{22}
   1.445    \item \isa {some_equality} (theorem), \bold{69}
   1.446 -  \item \isa {someI} (theorem), \bold{70}, \bold{75}
   1.447 +  \item \isa {someI} (theorem), \bold{70}
   1.448    \item \isa {someI2} (theorem), \bold{70}
   1.449 -  \item \isa {someI_ex} (theorem, \bold){71}
   1.450 +  \item \isa {someI_ex} (theorem), \bold{71}
   1.451    \item sort, \bold{150}
   1.452    \item \isa {spec} (theorem), \bold{64}
   1.453    \item \isa {split} (constant), \bold{137}
   1.454 @@ -578,11 +514,8 @@
   1.455    \item \isa {subsetI} (theorem), \bold{90}
   1.456    \item \isa {subst} (method), \hyperpage{61}
   1.457    \item substitution, \hyperpage{61--63}
   1.458 -  \item \isa {Suc}, \bold{20}
   1.459 -  \item \isa {Suc_leI} (theorem), \bold{171}
   1.460 -  \item \isa {Suc_Suc_cases} (theorem), \bold{115}
   1.461 +  \item \isa {Suc} (constant), \hyperpage{20}
   1.462    \item \isa {surj_def} (theorem), \bold{94}
   1.463 -  \item \isa {surj_f_inv_f} (theorem), \bold{94}
   1.464    \item surjections, \hyperpage{94}
   1.465    \item \isa {sym} (theorem), \bold{77}
   1.466    \item syntax translation, \bold{23}
   1.467 @@ -592,7 +525,7 @@
   1.468    \item tactic, \bold{10}
   1.469    \item tacticals, \hyperpage{82--83}
   1.470    \item term, \bold{3}
   1.471 -  \item \isa {term}, \bold{14}
   1.472 +  \item \isacommand {term} (command), \hyperpage{14}
   1.473    \item term rewriting, \bold{26}
   1.474    \item termination, \see{total function}{1}
   1.475    \item \isa {THEN} (attribute), \bold{77}, \hyperpage{79}, 
   1.476 @@ -602,17 +535,16 @@
   1.477    \item theory, \bold{2}
   1.478      \subitem abandon, \bold{14}
   1.479    \item theory file, \bold{2}
   1.480 -  \item \isa {thm}, \bold{14}
   1.481 -  \item \isa {tl}, \bold{15}
   1.482 +  \item \isacommand {thm} (command), \hyperpage{14}
   1.483 +  \item \isa {tl} (constant), \hyperpage{15}
   1.484    \item total function, \hyperpage{9}
   1.485    \item \isa {trace_simp}, \bold{31}
   1.486    \item tracing the simplifier, \bold{31}
   1.487 -  \item \isa {trancl_converse} (theorem), \bold{97}
   1.488    \item \isa {trancl_trans} (theorem), \bold{97}
   1.489 -  \item \isa {translations}, \bold{23}
   1.490 +  \item \isa {translations}, \bold{24}
   1.491    \item \isa {True}, \bold{3}
   1.492    \item tuple, \see{pair}{1}
   1.493 -  \item \isa {typ}, \bold{14}
   1.494 +  \item \isacommand {typ} (command), \hyperpage{14}
   1.495    \item type, \bold{2}
   1.496    \item type constraint, \bold{4}
   1.497    \item type declaration, \bold{150}
   1.498 @@ -622,7 +554,7 @@
   1.499    \item type variable, \bold{3}
   1.500    \item \isa {typedecl}, \bold{151}
   1.501    \item \isa {typedef}, \bold{151}
   1.502 -  \item \isa {types}, \bold{22}
   1.503 +  \item \isa {types}, \bold{23}
   1.504  
   1.505    \indexspace
   1.506  
   1.507 @@ -633,7 +565,7 @@
   1.508    \item \isa {UN_iff} (theorem), \bold{92}
   1.509    \item \isa {Un_subset_iff} (theorem), \bold{90}
   1.510    \item underdefined function, \hyperpage{165}
   1.511 -  \item \isa {undo}, \bold{14}
   1.512 +  \item \isacommand {undo} (command), \hyperpage{14}
   1.513    \item \isa {unfold}, \bold{28}
   1.514    \item unification, \hyperpage{60--63}
   1.515    \item \isa {UNION} (constant), \hyperpage{93}
   1.516 @@ -652,25 +584,11 @@
   1.517    \item variable, \bold{4}
   1.518      \subitem schematic, \bold{4}
   1.519      \subitem type, \bold{3}
   1.520 -  \item \isa {vimage_Compl} (theorem), \bold{95}
   1.521    \item \isa {vimage_def} (theorem), \bold{95}
   1.522  
   1.523    \indexspace
   1.524  
   1.525    \item \isa {wf_induct} (theorem), \bold{99}
   1.526 -  \item \isa {wf_inv_image} (theorem), \bold{99}
   1.527 -  \item \isa {wf_less_than} (theorem), \bold{98}
   1.528 -  \item \isa {wf_lex_prod} (theorem), \bold{99}
   1.529 -  \item \isa {wf_measure} (theorem), \bold{99}
   1.530    \item \isa {while}, \bold{167}
   1.531  
   1.532 -  \indexspace
   1.533 -
   1.534 -  \item \isa {zdiv_zadd1_eq} (theorem), \bold{135}
   1.535 -  \item \isa {zdiv_zmult1_eq} (theorem), \bold{135}
   1.536 -  \item \isa {zdiv_zmult2_eq} (theorem), \bold{135}
   1.537 -  \item \isa {zmod_zadd1_eq} (theorem), \bold{135}
   1.538 -  \item \isa {zmod_zmult1_eq} (theorem), \bold{135}
   1.539 -  \item \isa {zmod_zmult2_eq} (theorem), \bold{135}
   1.540 -
   1.541  \end{theindex}