\begin{theindex}

  \item \ml{-} (abbreviation, of \HOL\ theory part names), 170
  \item \ml{+} (addition, in \HOL\ logic), 185
  \item {\small\verb7+7} (addition, in \ML), 25, 29, \pin{53}
  \item {\small\verb+^+} (antiquotation, in \HOL\ logic), 156
  \item {\small\verb+:=+} (assignment, in \ML), 8, 25, 36
  \item {\small\verb+=+} (binding operator, in \ML), 24
  \item {\small\verb+(+$\cdots$\verb+)+} (brackets, in \ML), 24, 26
  \item {\small\verb+@+} (choice function, in \HOL\ logic), 147, 
		170, 171, 178
  \item \per $\cdots$ \per\ (comment markers, in \ML), 27
  \item \pes $\cdots$ \pee\ (comment markers, nested, in \ML), 27
  \item {\small\verb+/\+} (conjunction, in \HOL\ logic), 147, 171, 178
  \item {\small\verb+&+} (conjunction, in \ML), 25, 29, 36
  \item \ml{+} (disjoint union type operator, in HOL logic), 191
  \item {\small\verb:+:} (disjoint union type operator, in \ML), 21, 40
  \item {\small\verb+\/+} (disjunction, in \HOL\ logic), 147, 171, 178
  \item {\small\verb+/+} (division, in \ML), 25, 29, \pin{53}
  \item \ml{=} (equality, in \HOL\ logic), 147, 170
  \item {\small\verb+=+} (equality, in \ML), 25, 29, \pin{53}
  \item {\small\verb+$+} (escape, in \HOL\ logic parser), 147, 164
  \item {\small\verb+$+} (escape, in \ML\ parser), 55
  \item {\small\verb+\+} (escape, in \ML\ strings), 29, 211
  \item {\small\verb+?+} (existential quantifier, in \HOL\ logic), 147, 
		171, 178
  \item {\small\verb+?!+} (exists unique, in \HOL\ logic), 171, 178
  \item {\small\verb+?+} (failure trap, in \ML), 15, 26
  \item {\small\verb+!!+} (failure trap, iterative selective, in \ML), 
		17, 26
  \item {\small\verb+!+} (failure trap, iterative, in \ML), 17, 26
  \item {\small\verb+??+} (failure trap, selective, in \ML), 16, 26
  \item {\small\verb+\+} (function abstraction binder, in \HOL\ logic), 
		148, 211
  \item {\small\verb+\+} (function abstraction binder, in \ML), 14, 26, 
		38
  \item \ml{o} (function composition operator, in \HOL\ logic), 
		188--189
  \item {\small\verb+o+} (function composition operator, in \ML), 
		\pin{56}, 275
  \item \ml{->} (function type operator, in \HOL\ logic), 146, 178
  \item {\small\verb+->+} (function type operator, in \ML), 40
  \item \ml{>=} (greater or equal, in \HOL\ logic), 186
  \item \ml{>} (greater than, in \HOL\ logic), 186
  \item {\small\verb+>+} (greater than, in \ML), 25, 29, \pin{53}
  \item {\small\verb+==>+} (implication, in \HOL\ logic), 147, 170, 178
  \item \ml{<=} (less or equal, in \HOL\ logic), 186
  \item \ml{<} (less than, in \HOL\ logic), 185
  \item {\small\verb+<+} (less than, in \ML), 25, 29, \pin{53}
  \item {\small\verb+@+} (list concatenation, in \ML), 25, 29--30, 
		\pin{53}, 54, 58
  \item {\small\verb+.+} (list constructor, in \ML), 24, 25, 29, 
		\pin{53}
  \item \ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]} (lists, in \HOL\ logic), 
		186--188
  \item {\small\ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]}} (lists, in \ML), 
		12, 26
  \item {\small\verb+-+} (minus, in \ML), 25, 29
  \item \ml{*} (multiplication, in \HOL\ logic), 186
  \item {\small\verb+*+} (multiplication, in \ML), 25, 29, \pin{53}
  \item {\small\verb+~+} (negation, in \HOL\ logic), 147, 171, 178
  \item {\small\verb+-+} (`non-printable' symbol, in \ML), 9, 20, 50
  \item \ml{,} (pair constructor, in \HOL\ logic), 179
  \item {\small\verb+,+} (pair constructor, in \ML), 24, 25, 29, 36
  \item {\small\verb+#+} (product function operator, in \ML), \pin{56}
  \item {\small\verb+#+} (product type operator, in \HOL\ logic), 179
  \item {\small\verb+#+} (product type operator, in \ML), 9, 40
  \item {\small\verb+#+} (prompt, in \ML), 7, 85
  \item {\small\verb+;+} (sequencing, in \ML), 11, 26
  \item {\small\verb+^+} (string concatenation, in \ML), \pin{66}
  \item {\small\verb+`+ $\cdots$ \verb+`+} (string markers, in \ML), 13, 
		29
  \item \ml{-} (subtraction, in \HOL\ logic), 186
  \item {\small\verb+-+} (subtraction, in \ML), 25, 29, \pin{53}
  \item \ml{"$\cdots$"} (term quotes, in \ML), 144--146
  \item {\small\verb+;;+} (terminator, of \ML\ expressions), 7
  \item \ml{|-} (theorem marker, in \HOL\ logic), 159
  \item \ml{:} (type constraint, in \HOL\ logic), 143, 144
  \item {\small\verb+:+} (type constraint, in \ML), 24, 25, 32
  \item \ml{":$\cdots$"} (type quotes, in \ML), 144--146
  \item \ml{*,\,**,\,}$\ldots$ (type variables, in \HOL\ logic), 146
  \item {\small\verb+*+, \verb+**+,$\ldots$} (type variables, in \ML), 
		14, 40
  \item {\small\verb+!+} (universal quantifier, in \HOL\ logic), 147, 
		171, 178
  \item {\small\verb+<<+} (value comparison, in \ML), \pin{81}
  \item \verb+()+, \see{\ml{void}}{289}
  \item {\small\verb+_+} (wildcard, in \ML), 22, 24, 32, 34, 44
  \item \ml{0} ( zero, in \HOL\ logic), 181

  \indexspace

  \item abbreviation of types, in \HOL\ logic, 176
  \item abbreviation of types, in \ML, 17, 24, 40, 47
  \item \ml{abort\_when\_fail}, \pin{84}
  \item \ml{ABS}, 118, 119, \pin{174}
  \item \ml{ABS\_}$\ldots$, 195
  \item {\small\verb+abs_+$\ldots$}, 20, 49
  \item \ml{ABS\_CONV}, \pin{247}
  \item \ml{ABS\_REP\_THM}, 181
  \item {\small\verb+absrectype+}$\ldots${\small\verb+with+}$\ldots$, 
		24, 49--50
  \item abstract types, in \ML, 19--20, 40, 49--50
    \subitem listing current, 82
    \subitem printing of, 86--87
    \subitem reasons for, 48
  \item abstract-typed values, in \ML
    \subitem printing of, 20, 50
  \item abstraction rule, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem \ML\ function for, 174
  \item \ml{abstype}$\ldots$\ml{with}$\ldots$, 19--20, 49--50
  \item \ml{ACCEPT\_TAC}, 258, \pin{267}
  \item achievement, of goals, 258
  \item \ml{ADD}, 185, 186
  \item \ml{ADD\_ASSUM}, \pin{225}
  \item \ml{ADD\_CONV}, \pin{249}, 304
  \item \ml{ALL\_CONV}, \pin{246}
  \item \ml{ALL\_TAC}, 260, \pin{272}
  \item \ml{allowed\_constant}, \pin{208}
  \item alphanumerics, in \ML, 27--28
  \item alternation
    \subitem of conversions, 241--242
    \subitem of tactics, 273
  \item ancestry, of \HOL\ system theories, 160, 177
  \item {\small\verb+and+}, 24
  \item \ml{AND\_DEF}, 171
  \item antiquotation, in \HOL\ logic terms, 156, 176
  \item \ml{AP\_TERM}, 225, \pin{227}
  \item \ml{AP\_THM}, 225, \pin{227}
  \item \ml{append}, \pin{58}
  \item \ml{APPEND}, the constant in \HOL\ logic, 188
  \item \ml{APPEND}, the theorem in \HOL\ logic, 188
  \item \ml{append\_openw}, \pin{69}
  \item application, \see{function application}{289}
  \item \ml{ARB}, 149, 172, 179
  \item \ml{arithmetic}, 186
  \item arithmetic, in \HOL\ logic, 186
  \item arithmetic, in \ML, 82
  \item array, of assumptions, 282
  \item {\small ASCII}, 26, 92
  \item \ml{ascii}, \pin{52}
  \item \ml{ascii\_code}, \pin{52}
  \item \ml{ASM\_CASES\_TAC}, 270
  \item \ml{ASM\_REWRITE\_TAC}, 255, 271
  \item assignable variables, in \ML, 8, 11, 31, 33, 36, 47
  \item assignments, in \ML
    \subitem evaluation of, 36
    \subitem simultaneous, 9
    \subitem syntax of, 25
    \subitem type checking of, 44
  \item \ml{assoc}, \pin{62}
  \item \ml{associate\_restriction}, \pin{149}, 295
  \item associativity, of constructs in \ML, 10, 23, 26
    \subitem of infixes, 29
  \item \ml{ASSUM\_LIST}, 282, 287
  \item \ml{ASSUME}, \pin{173}, 220
  \item \ml{ASSUME\_TAC}, \pin{268}
  \item assumption introduction, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem \ML\ function for, 173
  \item assumption list, of goal, 258
  \item assumptions
    \subitem as array, 282
    \subitem as stack, 278
    \subitem compared methods of handling, 287
    \subitem denoting of, in proofs, 277, 280, 283
    \subitem discarding of, in proofs, 277, 279, 281
    \subitem explicit, 280
    \subitem importance of ordering of, 285
    \subitem internal, 286
    \subitem of sequents, 116
    \subitem of theorems, \see{hypothesis}{289}
    \subitem role of, in goal directed proof, 277
    \subitem tactic for adding, 268
  \item atomic types, in \HOL\ logic, 103
  \item \ml{autoload}, \pin{76}
  \item \ml{autoload\_theory}, \pin{79}, \pin{213}
  \item autoloading, \see{automatic loading}{289}
  \item automated derivation
    \subitem of case analysis theorems, 203
    \subitem of characterizing theorems for recursive types, 195
    \subitem of distinctness theorems, 203
    \subitem of one-to-one theorems, 203
    \subitem of recursive definitions, 198
    \subitem of structural induction tactics, 202
    \subitem of structural induction theorems, 201
  \item automatic loading, of \HOL\ theory components, 213
  \item \ml{auxiliary} library, 92
  \item \ml{axiom}, \pin{170}
  \item axiom of choice, 102
  \item axiom of infinity, 171, 172
    \subitem abstract form of, 123
  \item axiom of replacement, 102
  \item axioms
    \subitem abstract form of \HOL\ logic's, 123
    \subitem as inference rules, 119
    \subitem autoloading of, in \HOL\ system, 213
    \subitem declaration of, in \HOL\ logic, 162
    \subitem dispensibility of adding, 125, 172
    \subitem formal semantics of \HOL\ logic's, 122--123
    \subitem in \ml{bool} theory, 170, 180
    \subitem in \ml{ind} theory, 172
    \subitem in \ml{list} theory, 187
    \subitem in natural deduction, 158
    \subitem in \ml{num} theory, 181
    \subitem non-primitive, of \HOL\ logic, 170, 172, 180, 181, 187
    \subitem primitive, of \HOL\ logic, 170--172
    \subitem retrieval of, in \HOL\ system, 169--170
  \item \ml{axioms}, \pin{169}
  \item axioms, in a \HOL\ theory, 120

  \indexspace

  \item \ml{B}, \pin{56}
  \item \ml{b}, the subgoal package function, 267
  \item backtrace, 67
  \item \ml{backup}, \pin{266}
  \item \ml{backup\_limit}, 266
  \item \ml{bags} library, 92
  \item \ml{BASIC-HOL}, 177, 181
  \item \ml{basic-rewrites}, 254
  \item beta-conversion, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem \ML\ function for, 173
    \subitem not expressible as a theorem, 224, 240
  \item \ml{BETA\_CONV}, 118, 119, \pin{173}, 239
  \item \ml{BETA\_RULE}, \pin{244}
  \item bijection of types, in \HOL\ logic, 167
  \item binary tree theory, in \HOL\ logic, 197
  \item \ml{BINDERS}, 179
  \item \ml{binders}, \pin{169}
  \item binders, in \HOL\ logic, 148, 165
    \subitem declaration of, 162
    \subitem indicator functions for, 208
    \subitem parsing of, 152
    \subitem under interface maps, 207
  \item binding power, in \ML, 26
  \item bindings, in \ML
    \subitem abstract type, 19--20, 49
    \subitem concrete type, 17--19, 48
    \subitem effect of declarations on, 31
    \subitem evaluation of, 33--34
    \subitem in declarations, 7--8
    \subitem in function definitions, 11, 33--34
    \subitem kinds of, 33--34
    \subitem multiple, 34
    \subitem predeclared, 51--52
    \subitem scope of, 31
    \subitem simple, 33
    \subitem simultaneous, 8
    \subitem syntax of, 24
  \item \ml{bndvar}, 144
  \item BNF syntax, explanation of, 23
  \item \ml{body}, 144
  \item \ml{bool}, the \HOL\ theory, 170, 171, 177--180
  \item \ml{bool}, the type in \HOL\ logic, 142, 144, 170
  \item \ml{bool}, the type in \ML, 40, 41
  \item \ml{BOOL\_CASES\_AX}, 171
    \subitem abstract form of, 123
  \item boolean values, \see{truth values}{289}
  \item bound variables, in \HOL\ logic, 108
  \item breaks, in \ML\ pretty printing, 73
  \item \ml{butlast}, \pin{59}

  \indexspace

  \item \ml{C}, \pin{56}
  \item \ml{cached\_theories}, \pin{214}
  \item caching, 213
  \item \ml{can}, \pin{57}
  \item canonical contexts, in \HOL\ logic
    \subitem of terms, 109
    \subitem of types, 105
  \item cardinals library, 92
  \item carriage return
    \subitem after \ML\ expressions, 7
    \subitem in \ML\ expressions, 26
    \subitem in \ML\ strings, 29
  \item Carroll, J., 3
  \item Cartesian products, \see{product types}{289}
  \item case analysis, in \HOL\ logic
    \subitem as instance  of induction, 201, 204
    \subitem tactics for, 270
    \subitem theorems for, 203
  \item {\small\ml{case} $\cdots$ \ml{of} $\cdots$ \ml{|} $\cdots$}, 26
    \subitem relation to abstraction, 19, 26
  \item \ml{CB}, \pin{56}
  \item \ml{CCONTR}, 225, \pin{238}
  \item Centaur, 83, 94
  \item \ml{CHANGED\_CONV}, \pin{246}
  \item \ml{CHANGED\_TAC}, \pin{274}
  \item characteristic function, of type definitions, 131
  \item characteristic predicate, of type definitions, 166, 171
  \item characterizing theorem
    \subitem for defined types, 195
    \subitem for finitely-branching ordered trees, 190
    \subitem for lists, 187
    \subitem for numbers, 182
    \subitem use of, in deriving induction, 202
  \item choice axiom, 171
    \subitem abstract form of, 123
  \item choice operator, in \HOL\ logic, 170, 178
    \subitem abstract form of, 114
    \subitem formal semantics of, 114
    \subitem inference rules for, 232, 233
    \subitem primitive axiom for, 171
    \subitem syntax of, 147
  \item \ml{CHOOSE}, 225, \pin{234}
  \item \ml{CHOOSE\_THEN}, \pin{288}
  \item \ml{chop\_list}, \pin{63}
  \item Church, A., 101, 170, 171
  \item \ml{close}, \pin{70}
  \item \ml{close\_theory}, \pin{163}, 169
  \item \ml{Co}, \pin{56}
  \item \ml{combin}, 188
  \item combinations, in \HOL\ logic
    \subitem abbreviation for multiple, 148
    \subitem abstract form of, 107
    \subitem constructor for, 143
    \subitem destructor for, 143
    \subitem formal semantics of, 110
    \subitem quotation of, 146
  \item combinations, in \ML, 36, 44
  \item combinators, in \HOL\ logic, 188
  \item combinators, in \ML, 55--56
  \item \ml{combine}, \pin{64}
  \item \ml{COMMA\_DEF}, 180
  \item comments, in \ML, 27
  \item Common Lisp \HOL, 3, 72, 76, 84
  \item compilation, in \ML, 84
  \item \ml{compile}, \pin{72}
  \item \ml{compile\_on\_the\_fly}, 72, \pin{84}
  \item \ml{compilef}, \pin{72}
  \item \ml{compilet}, \pin{72}
  \item compound monotypes, in \ML, 41
  \item compound tactics, in \HOL\ system, 273
  \item compound types, in \HOL\ logic
    \subitem abstract form of, 103
    \subitem constructors for, 142, 146
    \subitem destructors for, 142
  \item computation phase, of proof search, 264
  \item \ml{concat}, \pin{66}
  \item concatenation, of lists
    \subitem in \HOL\ logic, 188
    \subitem in \ML, 25, 29, 30, 53, 54, 58
  \item concatenation, of \ML\ strings, 66
  \item \ml{concatl}, \pin{66}
  \item \ml{concl}, \pin{158}
  \item conclusions
    \subitem of inference rules, 117, 173
    \subitem of sequents, 116, 158
    \subitem of theorems, 158
  \item concrete recursive types, in \HOL\ logic, 193
  \item concrete types, in \ML, 17, 40, 48
  \item \ml{COND}, 147, 148, 151, 172, 179
  \item \ml{COND\_DEF}, 172
  \item conditional/loop construct, in \ML, 11--12, 25, 44
    \subitem evaluation of, 36--37
    \subitem syntax of, 25
    \subitem type checking of, 44
  \item conditional predicate, in \HOL\ logic, 147, 151
    \subitem definitional axiom for, 172
  \item conditionals, in \HOL\ logic, 147, 151, 172
  \item \ml{CONJ}, 225, \pin{235}
  \item \ml{CONJ\_TAC}, 260, \pin{269}
    \subitem \ML\ implementation of, 262
  \item \ml{CONJUNCT1}, 225, \pin{236}
  \item \ml{CONJUNCT2}, 225, \pin{236}
  \item conjunction, in \HOL\ logic, 178
    \subitem abstract form of, 121, 126
    \subitem constructor for, 147
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem inference rule for, 235
    \subitem syntax of, 147
    \subitem tactic for splitting of, 269
  \item conjunction, in \ML, 25, 36
  \item \ml{CONS}, 186
  \item \ml{CONS\_{11}}, 187
  \item consistency, of \HOL\ logic, 159, 259--260
    \subitem under constant specification, 127, 128
    \subitem under type definition, 130
  \item consistent theory, 124
  \item constant definition, 125
  \item constant definition extension, of \HOL\ logic
    \subitem abstract form of, 125
    \subitem \ML\ function for, 163--164
  \item constant expressions, in \ML, 29, 33, 35, 43
  \item constant specification, 127
  \item constant specification extension, of \HOL\ logic
    \subitem abstract form of, 127
    \subitem \ML\ function for, 165
  \item constant specifications, in \HOL\ logic
    \subitem autoloading of, 213
  \item \ml{constants}, \pin{169}
  \item constants, in \HOL\ logic
    \subitem abbreviational, 179
    \subitem abstract form of, 107
    \subitem constructor for, 143
    \subitem declaration of, 162
    \subitem destructor for, 143
    \subitem for pairs, 179
    \subitem for type definitions, 179
    \subitem formal semantics of, 110
    \subitem hiding status of, 212
    \subitem indicator function for, 208
    \subitem logical, 178
    \subitem primitive logical, 170
    \subitem primitive, abstract form of, 113
    \subitem supressing parsing behaviour of, 147
    \subitem system, 179
  \item constructions, in \ML, 24, 34, 36, 48
  \item constructors, in \ML, 25, 29
    \subitem type checking of, 43
  \item constructors, of concrete types in \HOL\ logic
    \subitem proving distinct, 203
    \subitem proving one-to-one, 203
  \item contexts, in semantics of \HOL\ logic, 108
  \item contradiction rule, in \HOL\ logic, 238
  \item \ml{CONV\_RULE}, \pin{244}
  \item \ml{CONV\_TAC}, \pin{244}
  \item conversion and unwinding library, 92
  \item conversions
    \subitem application specific, 239
    \subitem as families of equations, 240
    \subitem functions for building, 245--248
    \subitem implementation of, in \ML, 247--248
    \subitem operators on, 241--245
    \subitem purpose of, 239
    \subitem quantifier movement, 252, 307
    \subitem reduction by, 241
  \item \ml{convert} library, 92
  \item core images, saving of, 76
  \item counting inferences, in \HOL\ proofs, 205, 215, 220, 221, 223
  \item \ml{current\_theory}, \pin{161}
  \item \ml{CURRY}, 179
  \item \ml{curry}, \pin{57}
  \item currying, in \ML, 38, 52
    \subitem in primitive recursive definitions, 184
    \subitem in recursive definitions, 198
  \item customization of \HOL\ system, 83, 85, 211--212

  \indexspace

  \item debugging, of tactics, 263, 265
  \item declarations, in \ML
    \subitem at top level, 31
    \subitem effect on \ml{it}, 8
    \subitem evaluation of, 38
    \subitem local, 8, 26, 38
    \subitem relation to function abstraction, 14
    \subitem syntax of, 24
    \subitem type checking of, 45
  \item declared constants, in \HOL\ logic, 147, 164
  \item decomposition phase, of proof search, 264
  \item deductive systems, 117, 158
  \item $\ldots$\ml{\_DEF}, 184
  \item default print depth, for \HOL\ logic, 214
  \item default types, in \HOL\ logic, 206--207
  \item \ml{define\_finite\_set\_syntax}, \pin{154}, 297
  \item \ml{define\_new\_type\_bijections}, \pin{167}
  \item \ml{define\_set\_abstraction\_syntax}, \pin{154}, 297
  \item \ml{define\_type}, \pin{193}, 194, 198, 202
  \item defined types in \ML
    \subitem flag for printing, 84
    \subitem printing of, 82
  \item defining mechanisms, for \HOL\ logic, 163, 164
  \item \ml{definition}, \pin{170}
  \item definitional axioms, 166, 192
  \item definitional extension, of \HOL\ logic, 163
  \item definitional theories, 172
  \item \ml{definitions}, \pin{169}
  \item definitions, adding to \HOL\ logic, 164
  \item \ml{delete\_cache}, \pin{213}
  \item denoting assumptions, 277, 280, 283
  \item dependent types in \HOL\ logic, 148, 295
  \item \ml{DEPTH\_CONV}, \pin{243}, 248
    \subitem search strategy of, 243
    \subitem use of, in rewriting tools, 254
  \item derived rules, in \HOL\ logic
    \subitem importance of, 220
    \subitem justification of, 221
    \subitem list and derivations of some, 225--238
    \subitem list of axiomatic, 225
    \subitem pre-defined, 223--224
  \item \ml{dest\_abs}, \pin{144}
  \item \ml{dest\_comb}, \pin{144}
  \item \ml{dest\_const}, \pin{144}
  \item \ml{dest\_thm}, \pin{158}
  \item \ml{dest\_type}, \pin{142}
  \item \ml{dest\_var}, \pin {144}
  \item \ml{dest\_vartype}, \pin{142}
  \item Dhingra, I., 3
  \item discarding assumptions, 277, 279, 281
  \item \ml{DISCH}, 119, \pin{175}
  \item \ml{DISCH\_TAC}, \pin{269}, 278
  \item discharging assumptions, in \HOL\ logic
    \subitem abstract form of, 119
    \subitem \ML\ function for, 175
  \item \ml{DISJ1}, 225, \pin{236}
  \item \ml{DISJ2}, 225, \pin{237}
  \item \ml{DISJ\_CASES}, 225, \pin{237}
  \item \ml{DISJ\_CASES\_TAC}, \pin{270}
  \item disjoint union theory, in \HOL\ logic, 191
  \item disjoint union, in \ML, 21, 40
  \item disjunction, in \HOL\ logic, 178
    \subitem abstract form of, 121, 126
    \subitem constructor for, 147
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem inference rule for, 236--238
    \subitem syntax of, 148
    \subitem tactic for case splits on, 270
  \item disjunction, in \ML, 25, 36
  \item \ml{distinct}, \pin{65}
  \item \ml{DIV}, 186
  \item \ml{do}, 25, 29, \pin{53}
  \item dollared infixes, in \ML, 53, 55
  \item draft mode, in \HOL\ system, 161, 163, 169, 195, 208
  \item \ml{draft\_mode}, \pin{208}

  \indexspace

  \item \ml{e}, the subgoal package function, 267
  \item \ml{el}, \pin{58}
  \item \ml{EL}, the constant in \HOL\ logic, 188
  \item \ml{EL}, the theorem in \HOL\ logic, 188
  \item emacs, 85
  \item empty, \see{\ml{void}}{289}
  \item environments, in \ML\ evaluations, 31, 35--38
  \item epsilon operator, 114, 171
  \item \ml{EQ\_IMP\_RULE}, 225, \pin{228}
  \item \ml{EQ\_MP}, 225, \pin{227}
  \item \ml{EQ\_TAC}, \pin{272}
  \item \ml{EQT\_ELIM}, \pin{228}
  \item \ml{EQT\_INTRO}, 225, \pin{229}
  \item equality, in \HOL\ logic, 170, 171, 178
    \subitem abstract form of, 114
    \subitem formal semantics of, 113
    \subitem \ml{MP} rule for, 227
    \subitem other rules for, 228--230
    \subitem primitive axiom for, 171
    \subitem symmetry rule for, 226
    \subitem syntax of, 147
    \subitem tactic for splitting, 272
    \subitem transitivity rule for, 226
  \item equality, in \ML
    \subitem at function types, 53
    \subitem syntax of, 25
    \subitem weakness of, 53
  \item equational theorems, in \HOL\ logic
    \subitem produced by conversions, 239, 240
    \subitem use of in rewriting, 222
  \item equiv., 23
  \item \ml{ETA\_AX}, 171
    \subitem abstract form of, 123
  \item \ml{ETA\_CONV}, 225, \pin{231}
  \item \ml{eval} library, 92
  \item evaluation, of \ML\ constructs, 31
    \subitem control flow in, 32, 36--37
    \subitem counting inference invoked by, 84
    \subitem termination of, 35
    \subitem timing of, 84
  \item \ml{EVERY}, the \HOL\ constant, 188
  \item \ml{EVERY}, the \ML\ function, \pin{276}
  \item \ml{EVERY\_ASSUM}, 285
  \item \ml{EVERY\_CONV}, \pin{246}
  \item \ml{EVERY\_DEF}, 188
  \item existential quantifier, in \HOL\ logic, 178
    \subitem abbreviation for multiple, 121, 148
    \subitem abstract form of, 114, 121, 126
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem in infinity axiom, 172
    \subitem inference rules for, 233--234
    \subitem syntax of, 147
    \subitem tactic for, 273
  \item \ml{EXISTS}, 225, \pin{233}
  \item \ml{exists}, \pin{61}
  \item exists unique, in \HOL\ logic, 171
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
  \item \ml{EXISTS\_DEF}, 171
  \item \ml{EXISTS\_TAC}, \pin{273}
  \item \ml{EXISTS\_UNIQUE\_DEF}, 171
  \item exiting of \HOL\ system, 163
  \item \ml{EXP}, 186
  \item \ml{expand}, \pin{266}
  \item \ml{explode}, \pin{52}
  \item expressions, in \ML
    \subitem carriage return after, 7
    \subitem evaluation of, 35--38
    \subitem syntax of, 25
    \subitem terminator for, 7
    \subitem type checking of, 44
  \item \ml{EXT}, 225, \pin{232}
  \item \ml{extend\_theory}, \pin{169}
  \item extension, of \HOL\ logic, 192
    \subitem abstract form of, 124
    \subitem by constant definition, 125--126, 163
    \subitem by constant specification, 127--129, 165
    \subitem by type definition, 130--132, 166--167, 192--204
    \subitem by type specification, 132--136
    \subitem definitional, 163
  \item extension, of theory, 124
  \item extensionality rule, in \HOL\ logic, 232

  \indexspace

  \item \ml{F}, 178
    \subitem abstract form of, 121, 126
    \subitem axiom for, 159, 171
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem rules of inference for, 238
  \item \ml{F\_DEF}, 171
  \item {\small\verb+fail+}, 25
  \item failure strings, in \ML, 15--17
    \subitem for division by zero, 53
    \subitem of general purpose functions, 55
    \subitem of primitive identifiers, 51
  \item failure, in \ML, 15--17, 31--32, 35--37
    \subitem backtrace functions for, 67
    \subitem catch-all trap for, 16
    \subitem constructs for, 36--37
    \subitem explicit, 31
    \subitem implicit, 31
    \subitem iterative selective trapping of, 17, 26, 37, 45
    \subitem iterative trapping of, 17, 26, 37, 45
    \subitem selective trapping of, 16, 26, 37, 45
    \subitem side effects of, 35
    \subitem similar, 31
    \subitem test for, 57
    \subitem to cause exit from \HOL, 84
    \subitem trapping of, 15, 26, 37, 45
  \item failure, of tactics, 259--260, 263--265, 288
    \subitem debugging, 263
  \item \ml{failwith}, 15, 25, 31, 36, 44
  \item \ml{false}, 29, 43
  \item falsity, in \HOL\ logic, \see{\ml{F}}{289}
  \item families of inferences, in \HOL\ logic, 173, 224, 240
  \item \ml{fast\_arith}, \pin{82}
  \item \ml{FCOND}, 179
  \item \ml{file\_load\_msg}, \pin{84}
  \item \ml{filter}, \pin{62}
  \item \ml{FILTER\_ASM\_REWRITE\_TAC}, 271
  \item \ml{find}, \pin{61}
  \item \ml{find\_file}, \pin{70}
  \item \ml{find\_ml\_file}, \pin{71}
  \item \ml{find\_theory}, \pin{71}
  \item \ml{finite\_sets} library, 92
  \item \ml{FIRST}, \pin{274}
  \item \ml{FIRST\_ASSUM}, 285
  \item \ml{FIRST\_CONV}, \pin{245}
  \item fixed point theory library, 92
  \item \ml{fixpoints} library, 92
  \item flags, for subgoal package, 267
  \item flags, in \ML, 84, 205
  \item \ml{flat}, \pin{63}, 275
  \item \ml{FLAT}, the constant in \HOL\ logic, 188
  \item \ml{FLAT}, the theorem in \HOL\ logic, 188
  \item follows from, in natural deduction, 117, 158
  \item \ml{forall}, \pin{61}
  \item \ml{FORALL\_DEF}, 171
  \item form feed
    \subitem in \ML\ expressions, 26
    \subitem in \ML\ strings, 29
  \item formulas as terms, in \HOL\ logic, 114, 158
  \item forward proof
    \subitem compared to goal directed, 257
    \subitem interfacing to goal directed, 267
  \item Franz Lisp \HOL, 3, 72, 76, 84
  \item free variables, in \HOL\ logic, 229, 231--234
    \subitem abstract form of, 108
  \item free variables, in \ML
    \subitem binding of, 38
    \subitem in function definitions, 11
  \item \ml{fst}, \pin{51}
  \item \ml{FST}, the axiom in \HOL\ logic, 180
  \item \ml{FST}, the constant in \HOL\ logic, 179
    \subitem definition of, 180
  \item \ml{FST\_DEF}, 180
  \item {\ml{fun$\cdots$}\ml{|}\ml{$\cdots$}}, 18
    \subitem evaluation of, 38
    \subitem syntax of, 26
    \subitem type checking of, 45
  \item function (pattern) selection abstraction, in \ML, 18, 26, 38, 
		45
  \item function abstraction, in \HOL\ logic, 144
    \subitem abbreviation for multiple, 152
    \subitem abstract form of, 107
    \subitem changing symbol for, 211--212
    \subitem constructor for, 143
    \subitem destructor for, 143
    \subitem formal semantics of, 111
    \subitem inference rules for, 174
    \subitem paired, 152--153, 205
    \subitem pretty printing, of paired, 205
    \subitem relation to \ml{let}-terms, 153
    \subitem subterms of, 152
    \subitem symbol for, 146
    \subitem syntax of, 146
    \subitem type checking of, 146
    \subitem uncurrying, in paired, 152--153
  \item function abstraction, in \ML
    \subitem evaluation of, 38
    \subitem relation to declarations, 14
    \subitem syntax of, 26
    \subitem type checking of, 45
  \item function application, in \HOL\ logic
    \subitem abstract form of, 107
    \subitem associativity of, 108
    \subitem constructor for, 143, 146
    \subitem destructor for, 143
    \subitem formal semantics of, 110
    \subitem inference rules for, 227
    \subitem syntax of, 146
  \item function application, in \ML, 9
    \subitem associativity of, 10
    \subitem evaluation of, 36
    \subitem iteration of, 57
    \subitem partial, 10
    \subitem precedence of, 9
    \subitem syntax of, 25
    \subitem type checking of, 44
  \item function composition, in \HOL\ logic, 188--189
  \item function composition, in \ML, 56, 275
  \item function types, in \HOL\ logic
    \subitem abstract form of, 103
    \subitem constructors for, 142
    \subitem destructors for, 142
    \subitem formal semantics of, 105
  \item function types, in \ML, 40, 44
  \item functions in \ML, printing of, 9
  \item \ml{funpow}, \pin{57}

  \indexspace

  \item \ml{g}, the subgoal package function, 267
  \item \ml{GEN}, 225, \pin{230}
  \item \ml{GEN\_TAC}, \pin{268}
  \item generalization rule, in \HOL\ logic, 230
  \item generic types, in \HOL\ logic, 162
  \item generic types, in \ML, 42
  \item \ml{get\_flag\_value}, \pin{85}
  \item \ml{get\_state}, \pin{266}
  \item \ml{goal}, 259
  \item goal directed proof search
    \subitem composition phase of, 264
    \subitem concepts of, 258--261
    \subitem decomposition phase of, 264
    \subitem generation of proofs by, 262
    \subitem reason for, 257
  \item goals, in \HOL\ system, 258
  \item Gordon, M., 3
  \item \ml{group} library, 92
  \item group theory library, 92

  \indexspace

  \item has type {\it vs} possesses type, 42
  \item \ml{hd}, 12, 13, \pin{51}
  \item \ml{HD}, the constant in \HOL\ logic, 186
  \item \ml{HD}, the definition in \HOL\ logic, 188
  \item \ml{help}, \pin{87}, 294
  \item help system, 87--88, 294
  \item \ml{help\_search\_path}, \pin{88}, 294
  \item \ml{hide\_constant}, \pin{212}
  \item Hilbert, D., 171
  \item Hoare logic library, 92
  \item \ml{HOL}, 160, 170, 177
  \item \HOL\ system
    \subitem adjustment of user interface of, 204--212
    \subitem caching theories in, 213
    \subitem changeable symbols of, 211--212
    \subitem customization of, 85--87
    \subitem flags in, 84, 205
    \subitem help search path for, 88
    \subitem hiding constants in, 212
    \subitem interface maps in, 207--211
    \subitem library search path for, 90
    \subitem new interface for, 94--97
    \subitem non-Unix versions of, 80
    \subitem root directory of, 89
    \subitem search path for, 70--71, 89
    \subitem sticky types in, 206--207
    \subitem timing and counting inferences in, 215
    \subitem typical work in, 160
    \subitem version number of, 81
  \item \ml{hol-init.ml}, 80
  \item \ml{HOL\_DEFINITION}, 179
  \item \ml{host\_name}, \pin{81}
  \item Huet, G., 3, 178, 222
  \item \ml{hyp}, \pin{158}
  \item hypotheses
    \subitem of inference rules, 117
    \subitem of sequents, 117, 158
    \subitem of theorems, 158

  \indexspace

  \item \ml{I}, constant in \HOL\ logic, 188
  \item \ml{I}, the constant in \ML, \pin{55}
  \item \ml{I\_DEF}, 188
  \item \ml{I\_o\_ID}, 189
  \item \ml{I\_THM}, 189
  \item identifiers, in \HOL\ logic, 139--140
  \item identifiers, in \ML
    \subitem binding of, 51--54
    \subitem dollared, 53--54
    \subitem evaluation of, 35
    \subitem in expression evaluation, 34
    \subitem lexical aspects of, 27--28
    \subitem predeclared, 51--54
    \subitem type checking of, 43
  \item identity tactic, 260, 272
  \item {\small if $\cdots$ loop $\cdots$ else $\cdots$}, 12
    \subitem evaluation of, 36--37
    \subitem syntax of, 25
    \subitem type checking of, 44
  \item {\small if $\cdots$ loop $\cdots$ loop $\cdots$}, 25, 36--37
  \item {\small if $\cdots$ then $\cdots$ else $\cdots$}, 11--12, 25, 
		36
  \item {\small if $\cdots$ then $\cdots$ loop $\cdots$}, 11--12, 25, 
		36
  \item iff, in \HOL\ logic, 178
    \subitem definitional axiom for, 171
  \item \ml{IMP\_ANTISYM\_AX}, 171
    \subitem abstract form of, 123
  \item \ml{IMP\_RES\_TAC}, \pin{271}
  \item implication, in \HOL\ logic, 170, 178
    \subitem abstract form of, 114
    \subitem formal semantics of, 113
    \subitem inference rules for, 226, 228
    \subitem primitive axiom for, 171
    \subitem syntax of, 147
    \subitem tactics for, 269, 271
  \item \ml{implode}, \pin{52}
  \item {\small\verb+in+}, 26
  \item \ml{ind}, the theory, 172, 177
  \item \ml{ind}, the type, 172
  \item individuals, 172
  \item \ml{INDUCT}, 181
  \item \ml{INDUCT\_TAC}, 181, 202, 260
  \item \ml{INDUCT\_THEN}, \pin{202}
  \item \ml{INDUCTION}, 181
  \item induction rule
    \subitem for concrete recursive types, 201
    \subitem for lists, in \HOL\ logic, 187
    \subitem for numbers, in \HOL\ logic, 181
    \subitem for \ml{trees}, in \HOL\ logic, 190
    \subitem structural, derivation of, 200--201
  \item induction tactics, 260
    \subitem derivation of, 202--203
  \item inference rules, of \HOL\ logic
    \subitem abstract form of primitive, 117
    \subitem derived, 225--238
    \subitem formal semantics of, 119
    \subitem primitive, 173--175
    \subitem some not properly derived, 224--225
  \item inference schemes, in \HOL\ logic, 173
  \item inference, in natural deduction, 158
  \item inferences, in \HOL\ logic
    \subitem as \ML\ function applications, 220
    \subitem counting of, 205, 215
    \subitem in derived rules, 220
    \subitem in goal-directed proof search, 258, 264
    \subitem notation for, 173
  \item \ml{INFINITY\_AX}, 172
    \subitem abstract form of, 123
  \item \ml{infixes}, \pin{169}
  \item infixes, in \HOL\ logic, 147, 164
    \subitem declaration of, 164
    \subitem in recursive type definitions, 198
    \subitem indicator functions for, 208
    \subitem pretty printing of, 205
    \subitem primitive recursive definitions, 185
    \subitem under interface maps, 207
  \item infixes, in \ML, 29, 36, 53, 55
    \subitem currying of, 52
  \item \ml{INIT}
    \subitem abstract form of, 123
    \subitem as \ml{BASIC\_HOL}, 181
    \subitem formal semantics of, 123
  \item initial theory, of \HOL\ logic, 181
    \subitem abstract form of, 123
  \item initiality, 195
  \item initialization of \HOL, 80
  \item \ml{inject\_input}, \pin{79}
  \item \ml{inl}, 21, \pin{51}
  \item \ml{INL}, the constant in \HOL\ logic, 191
  \item \ml{INL}, the theorem in \HOL\ logic, 192
  \item \ml{inr}, 21, \pin{51}
  \item \ml{INR}, the constant in \HOL\ logic, 191
  \item \ml{INR}, the theorem in \HOL\ logic, 192
  \item \ml{INST\_TYPE}, 119, \pin{175}, 222
  \item \ml{install}, \pin{89}
  \item \ml{int}, 7, 40
  \item \ml{int\_of\_string}, \pin{52}
  \item \ml{integer} library, 92
  \item integers (as quotient types) library, 92
  \item integers (from groups) library, 92
  \item integers, in \ML, 29, 43
  \item interface maps, 205, 207--211
    \subitem in printing, 84
  \item interface, new, 94--97
  \item \ml{interface\_map}, \pin{208}
  \item \ml{interface\_print}, \pin{84}, 205, 208
  \item \ml{intersect}, \pin{64}
  \item \ml{INV\_SUC}, 181
  \item \ml{is\_alphanum}, \pin{28}, \pin{141}
  \item \ml{is\_binder}, \pin{208}
  \item \ml{is\_constant}, \pin{208}
  \item \ml{is\_hidden}, \pin{212}
  \item \ml{is\_infix}, \pin{208}
  \item \ml{is\_letter}, \pin{28}, \pin{140}
  \item \ml{IS\_PAIR}, 179
  \item \ml{IS\_PAIR\_DEF}, 180
  \item \ml{isl}, 21, \pin{51}
  \item \ml{ISL}, the constant in \HOL\ logic, 191
  \item \ml{ISL}, the theorem in \HOL\ logic, 191
  \item \ml{ISL\_OR\_ISR}, 191
  \item isomorphism of types, in \HOL\ logic, 181, 192
  \item \ml{isr}, 21
  \item \ml{ISR}, the constant in \HOL\ logic, 191
  \item \ml{ISR}, the theorem in \HOL\ logic, 191
  \item \ml{it}, 7, 8
  \item iterated function application, in \ML, 57
  \item \ml{itlist}, \pin{60}

  \indexspace

  \item justifications, in goal-directed proof search, 258
    \subitem \ml{THEN} example of, 276

  \indexspace

  \item \ml{K}, the constant in \HOL\ logic, 188
  \item \ml{K}, the constant in \ML, \pin{55}
  \item \ml{K\_DEF}, 188
  \item \ml{K\_THM}, 189
  \item \ml{KI}, \pin{56}

  \indexspace

  \item labelled \ml{tree} theory, in \HOL\ logic, 189--190
  \item lambda expressions, in \ML, 14--15
    \subitem extended form of, 18
  \item lambda symbol, in \HOL\ logic, resetting, 211
  \item lambda terms, in \HOL\ logic, 107
  \item \ml{last}, \pin{59}
  \item \LCF, 119, 144, 146, 170, 178, 179, 288
    \subitem Cambridge, 3, 222, 240, 264
    \subitem Edinburgh, 3, 222, 257, 278
  \item Leisenring, A., 171
  \item lemmas, 257, 271
  \item \ml{length}, \pin{58}, 275
  \item \ml{LENGTH}, the constant in \HOL\ logic, 188
  \item \ml{LENGTH}, the theorem in \HOL\ logic, 188
  \item \ml{LENGTH\_CONV}, \pin{250}, 304
  \item \ml{LESS}, 185
  \item less than, in \HOL\ logic, 185
  \item \ml{LET}, 153, 172, 179
  \item \ml{let} $\ldots$ \ml{in} $\ldots$, 7--8
    \subitem evaluation of, 33, 38
    \subitem syntax of, 24, 26
    \subitem type checking of, 43, 45
  \item \ml{let}, in \ML, 7
  \item \ml{let}-terms, in \HOL\ logic
    \subitem as abbreviations, 153
    \subitem constant for, 171, 179
    \subitem definitional axiom for, 171
    \subitem pretty printing of, 205
    \subitem simplification of, 250, 305
  \item \ml{let\_after}, \pin{77}
  \item \ml{let\_before}, \pin{77}
  \item \ml{let\_CONV}, \pin{250}, 305
  \item \ml{LET\_DEF}, 172
  \item \ml{letrec} $\ldots$ \ml{in} $\ldots$, 11
    \subitem evaluation of, 33, 38
    \subitem syntax of, 24, 26
    \subitem type checking of, 43, 45
  \item \ml{letref} $\ldots$ \ml{in} $\ldots$, 8
    \subitem evaluation of, 33, 38
    \subitem syntax of, 24, 26
    \subitem type checking of, 43, 45
  \item letters, in \ML, 27
  \item {\small\verb+lettype+}, 17, 24, 40, 47--48
  \item \ml{lhs}, 144
  \item libraries
    \subitem directory of, 93
    \subitem installation of, 94
    \subitem load files for, 90--91, 93
    \subitem loading of, 84
  \item \ml{libraries}, \pin{90}
  \item \ml{library\_pathname}, \pin{92}, 293
  \item \ml{library\_search\_path}, \pin{90}
  \item line feed
    \subitem in \ML\ expressions, 26
    \subitem in \ML\ strings, 29
  \item \ml{link}, \pin{81}
  \item Lisp
    \subitem accessing of, from \HOL\ system, 82
    \subitem core images, 76
  \item \ml{lisp}, \pin{82}
  \item list concatenation, in \ML, 12
    \subitem parser status of, 54
  \item list constructor, in \ML, 12, 29, 53
    \subitem in expression evaluation, 35
    \subitem syntax of, 24, 25
    \subitem type checking of, 44
  \item list definitions, in \HOL\ logic, 188
  \item list theorems, in \HOL\ logic, 187--188
  \item \ml{list} theory, in \HOL\ logic, 186--188
  \item \ml{list}, the type operator in \HOL\ logic, 186
  \item \ml{list}, the type operator in \ML, 40
  \item \ml{list\_Axiom}, 187
  \item \ml{list\_CASES}, 187
  \item \ml{list\_EQ\_CONV}, \pin{250}, 304
  \item \ml{LIST\_INDUCT}, 187
  \item \ml{list\_INDUCT}, 187
  \item \ml{LIST\_INDUCT\_TAC}, 187
  \item \ml{list\_mk\_abs}, \pin{148}
  \item \ml{list\_mk\_comb}, \pin{148}
  \item \ml{list\_mk\_conj}, 148
  \item \ml{list\_mk\_disj}, 148
  \item \ml{list\_mk\_exists}, \pin{148}
  \item \ml{list\_mk\_forall}, \pin{148}
  \item \ml{list\_mk\_imp}, 148
  \item \ml{list\_mk\_pair}, 148
  \item lists, in \HOL\ logic, 186--188
  \item lists, in \ML
    \subitem evaluation of, 38
    \subitem in expression evaluation, 35
    \subitem syntax of, 24, 26
    \subitem type checking of, 45
  \item \ml{load}, \pin{71}, 90
  \item \ml{load\_library}, \pin{90}
  \item \ml{load\_theory}, \pin{169}
  \item \ml{loadf}, \pin{71}
  \item loading, of \HOL\ theories, 213
  \item \ml{loadt}, \pin{71}
  \item locations, 31, 36
  \item \ml{LOG}, 121
    \subitem formal semantics of, 122
  \item logical constants, in \HOL\ logic, 171, 178
  \item $\ldots$\ml{ltree}, 190
  \item \ml{ltree}, the \HOL\ theory, 189--190
  \item \ml{ltree\_Axiom}, 190
  \item \ml{ltree\_Induct}, 190

  \indexspace

  \item \ml{map}, 14, \pin{59}, 274
  \item \ml{MAP}, the constant in \HOL\ logic, 188
  \item \ml{MAP}, the theorem in \HOL\ logic, 188
  \item \ml{MAP\_EVERY}, 202
  \item \ml{mapfilter}, \pin{62}
  \item \ml{mapshape}, 275
  \item matching, of patterns, in \ML, 34--35
  \item \ml{max\_print\_depth}, \pin{75}, \pin{214}
  \item Melham, T., 3, 189
  \item \ml{mem}, \pin{61}
  \item Milner, R., 3, 139, 145, 222, 257, 274
  \item \ml{MIN}, 120
  \item minimal theory, of \HOL\ logic, 120
  \item \ml{MK\_ABS}, 225, \pin{247}
  \item \ml{mk\_abs}, \pin{143}, 146
  \item \ml{MK\_COMB}, 225, \pin{247}
  \item \ml{mk\_comb}, \pin{143}, 146
  \item \ml{mk\_cond}, 147
  \item \ml{mk\_conj}, 147
  \item \ml{mk\_cons}, 148
  \item \ml{mk\_const}, \pin{143}, 146
  \item \ml{mk\_disj}, 147
  \item \ml{mk\_eq}, 147
  \item \ml{mk\_exists}, 147
  \item \ml{mk\_forall}, 147
  \item \ml{mk\_imp}, 147
  \item \ml{mk\_let}, 147
  \item \ml{mk\_list}, 148
  \item \ml{mk\_neg}, 147
  \item \ml{MK\_PAIR}, 179
  \item \ml{mk\_pair}, 148
  \item \ml{MK\_PAIR\_DEF}, 180
  \item \ml{mk\_select}, 147
  \item \ml{mk\_type}, \pin{142}, 146
  \item \ml{mk\_var}, \pin{143}, 146
  \item \ml{mk\_vartype}, \pin{142}, 146
  \item \ML
    \subitem arithmetic in, 82
    \subitem \verb+CAML+ version of, 3
    \subitem constant expressions in, 29
    \subitem \HOL\ version of, 3
    \subitem identifiers in, 27--30
    \subitem original version of, 3
    \subitem pretty printer for, 72--75, 214
    \subitem prompt character of, 7, 84, 85
    \subitem purpose of, in \HOL\ system, 278
    \subitem short form of syntax of, 32
    \subitem special symbols of, 27--28
    \subitem Standard, 3
    \subitem syntax of bindings in, 24
    \subitem syntax of declarations in, 24
    \subitem syntax of expressions in, 25--26
    \subitem syntax of patterns in, 24
    \subitem top level expression terminator in, 7
    \subitem top level of, 7, 31, 42, 50, 84, 85
    \subitem type checking of, 32, 42--45
    \subitem versions of, 3
  \item \ml{ml\_curried\_infix}, \pin{52}
  \item \ML\ml{\_eval}, \pin{79}
  \item \ml{ml\_paired\_infix}, \pin{52}
  \item \ml{MOD}, 186
  \item Modus Ponens, in \HOL\ logic
    \subitem abstract form of, 119
    \subitem \ML\ function for, 175
  \item monotonicity, in deductive systems, 117
  \item Morris, L., 3, 47
  \item \ml{MP}, 119, \pin{175}
  \item \ml{MULT}, 186
  \item multiple bindings, in \ML, 34

  \indexspace

  \item natural deduction, 158
  \item natural numbers, \see{number theory}{289}
  \item negation, in \HOL\ logic
    \subitem abstract form of, 121, 126
    \subitem constructor for, 147
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem syntax of, 147
  \item \ml{new\_}$\ldots$, 169
  \item \ml{new\_alphanum}, \pin{28}, \pin{141}
  \item \ml{new\_axiom}, \pin{162}
  \item \ml{new\_binder}, \pin{162}
  \item \ml{new\_binder\_definition}, \pin{164}
  \item \ml{new\_constant}, \pin{162}
  \item \ml{new\_definition}, \pin{164}
  \item \ml{new\_flag}, \pin{85}
  \item \ml{new\_infix}, \pin{162}
  \item \ml{new\_infix\_definition}, \pin{164}
  \item \ml{new\_infix\_list\_rec\_definition}, 187
  \item \ml{new\_infix\_prim\_rec\_definition}, \pin{183}, 185
  \item \ml{new\_letter}, \pin{28}, \pin{140}
  \item \ml{new\_list\_rec\_definition}, \pin{187}
  \item \ml{new\_parent}, \pin{161}
  \item \ml{new\_prim\_rec\_definition}, \pin{183}, 197
  \item \ml{new\_recursive\_definition}, \pin{198}
  \item \ml{new\_special\_symbol}, \pin{28}, \pin{141}
  \item \ml{new\_specification}, \pin{165}
  \item \ml{new\_syntax\_block}, \pin{89}, 301
  \item \ml{new\_theory}, \pin{161}
  \item \ml{new\_type}, \pin{162}
  \item \ml{new\_type\_abbrev}, \pin{176}
  \item \ml{new\_type\_definition}, \pin{166}, 192
  \item \ml{NIL}, 186
  \item \ml{NO\_CONV}, \pin{245}
  \item \ml{NO\_TAC}, \pin{272}
  \item \ml{Node}, 190
  \item \ml{node}, 189
  \item \ml{Node\_{11}}, 190
  \item \ml{node\_{11}}, 190
  \item non-printable values in \ML, 9, 20, 50
  \item \ml{not}, 25, 29, \pin{53}
  \item \ml{NOT\_CONS\_NIL}, 187
  \item \ml{NOT\_DEF}, 171
  \item \ml{NOT\_NIL\_CONS}, 187
  \item \ml{NOT\_SUC}, 181
  \item notation
    \subitem for specification of rules, 173
    \subitem for specification of tactics, 260
  \item \ml{null}, 12, \pin{51}
  \item \ml{NULL}, the constant in \HOL\ logic, 186
  \item \ml{NULL}, the definition in \HOL\ logic, 188
  \item \ml{num}, the theory in \HOL\ logic, 181
  \item \ml{num}, the type in \HOL\ logic, 181
  \item \ml{num\_Axiom}, 182, 197
  \item \ml{num\_CONV}, \pin{181}, 225
  \item \ml{num\_EQ\_CONV}, \pin{249}, 304
  \item number theory, in \HOL\ logic, 186
    \subitem type definition package version of, 196

  \indexspace

  \item \ml{ONCE\_DEPTH\_CONV}, \pin{244}
  \item \ml{one}, the \HOL\ theorem, 192
  \item \ml{one}, the \HOL\ theory, 192
  \item \ml{one}, the \HOL\ type, 192
  \item one-to-one predicate, in \HOL\ logic
    \subitem abstract form of, 121, 126
    \subitem definitional axiom for, 172
    \subitem formal semantics of, 123
    \subitem in \ml{bool} theory, 178
  \item \ml{one\_Axiom}, 192
  \item \ml{one\_axiom}, 192
  \item \ml{ONE\_ONE\_DEF}, 172
  \item onto predicate, in \HOL\ logic
    \subitem abstract form of, 121, 126
    \subitem definitional axiom for, 172
    \subitem formal semantics of, 123
    \subitem in \ml{bool} theory, 178
  \item \ml{ONTO\_DEF}, 172
  \item \ml{openi}, \pin{69}
  \item \ml{openw}, \pin{69}
  \item operating systems functions, from \HOL, 80--81
  \item \ml{or}, 25, 36
    \subitem not a dollared infix, 29
  \item \ml{OR\_DEF}, 171
  \item ordinary variables, in \ML, 33, 35
  \item \ml{ORELSE}, \pin{273}
  \item \ml{ORELSEC}, \pin{241}, 245
  \item \ml{outl}, 21, \pin{51}
  \item \ml{OUTL}, the constant in \HOL\ logic, 191
  \item \ml{OUTL}, the theorem in \HOL\ logic, 192
  \item \ml{outr}, 21, \pin{51}
  \item \ml{OUTR}, the constant in \HOL\ logic, 191
  \item \ml{OUTR}, the theorem in \HOL\ logic, 192

  \indexspace

  \item \ml{p}, the subgoal package function, 267
  \item \ml{PAIR}, 180
  \item \ml{PAIR\_EQ}, 180
  \item \ml{PAIR\_EXISTS}, 180
  \item \ml{PAIRED\_BETA\_CONV}, \pin{249}, 303
  \item pairing constructor, in \HOL\ logic, 179
    \subitem associativity of, 179
    \subitem definition of, 180
  \item pairs, in \HOL\ logic, 179--180
    \subitem in abstractions, 152--153
  \item pairs, in \ML, 9
    \subitem evaluation of, 36
    \subitem in expression evaluation, 35
    \subitem syntax of, 24, 25
    \subitem type checking of, 44
  \item \ml{parents}, \pin{169}
  \item parents, of \HOL\ theories, 160
  \item \ml{parser} library, 92
  \item parsing, of \HOL\ logic
    \subitem hiding constant status in, 212
    \subitem of binders, 152
    \subitem of conditionals, 151
    \subitem of constants, before definition, 164
    \subitem of function abstractions, 152
    \subitem of \ml{let}-terms, 153
    \subitem of list expressions, 187
    \subitem of pairs, 179
    \subitem of quotation syntax, 144, 152
    \subitem of standard notations, 147
    \subitem of sum types, 191
  \item partial function application, in \ML, 10
  \item \ml{partition}, \pin{63}
  \item pattern matching, in \ML\ evaluations, 34--35
  \item pattern selection abstraction, 
		\see{function selection abstraction}{289}
  \item patterns, in \ML, 19
    \subitem matching with values, 34--35
    \subitem syntax of, 24
    \subitem type checking of, 43--44
  \item Paulson, L., 3, 178, 222, 264
  \item Peano's axioms, 181, 182, 190
  \item polymorphic terms, in \HOL\ logic, 108
  \item polymorphic types, in \HOL\ logic, 105
    \subitem formal semantics of, 106
  \item polymorphism, in \ML, 13--14, 39
  \item \ml{POP\_ASSUM}, \pin{278}
  \item \ml{POP\_ASSUM\_LIST}, 284
  \item popping, of assumptions, 278
  \item ports, in \ML\ input-output, 69
  \item \ml{PPLAMB}, 178
  \item \ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system, 
		119, 182
  \item precedence, in \HOL\ logic
    \subitem under interface maps, 207
  \item precedence, in \ML, 23
    \subitem of function application in \ML, 9
    \subitem of infixes, in \ML, 29
    \subitem of prefixes, in \ML, 29
    \subitem of while construct, in \ML, 11
  \item precision, in \ML\ arithmetic, 82--83
  \item \ml{pred\_sets} library, 92
  \item predeclared bindings, in \ML, 51--54
  \item prefixes, in \ML, 29--30, 36, 44, 53--54
  \item \ml{preterm}, 302
    \subitem the flag, \pin{84}
    \subitem the type, 157
  \item \ml{preterm\_handler}, \pin{157}, 303
  \item \ml{preterm\_to\_term}, \pin{157}, 302
  \item preterms, 156--157, 302
  \item pretty printing
    \subitem flags for, in \HOL\ system, 84, 205
    \subitem of \ML, 72--75
  \item \ml{prettyp} library, 92
  \item \ml{prim\_rec}, 182--185, 197
  \item primitive constants, of \HOL\ logic, 109, 113, 170, 178
  \item primitive inference, in natural deduction, 158
  \item primitive inferences, of \HOL\ logic, 
		\see{inference rules}{289}
  \item primitive recursion theorem
    \subitem a degenerate case, 196
    \subitem automated use of, in \HOL\ system, 182--185, 187, 197--198
    \subitem for binary trees, 197--200
    \subitem for lists, 187
    \subitem for numbers, 182--185
  \item primitive recursive definitions, in \HOL\ logic
    \subitem automated, 182--185
    \subitem justification of, 182
  \item primitive recursive functions, 182
  \item \ml{print\_all\_subgoals}, \pin{84}
  \item \ml{print\_all\_thm}, \pin{73}, 159
  \item \ml{print\_begin}, \pin{73}
  \item \ml{print\_bool}, \pin{73}
  \item \ml{print\_break}, \pin{74}
  \item \ml{print\_cond}, \pin{84}, 205
  \item \ml{print\_defined\_types}, \pin{82}
  \item \ml{print\_end}, \pin{73}
  \item \ml{print\_fasl}, \pin{84}
  \item \ml{print\_ibegin}, \pin{73}
  \item \ml{print\_infix}, \pin{84}, 205
  \item \ml{print\_int}, \pin{73}
  \item \ml{print\_let}, 83, \pin{84}, 205
  \item \ml{print\_lettypes}, 82, \pin{84}
  \item \ml{print\_lib}, \pin{84}, 90
  \item \ml{print\_list}, \pin{74}, 84, 205
  \item \ml{print\_load}, \pin{84}
  \item \ml{print\_newline}, \pin{74}
  \item \ml{print\_quant}, \pin{84}, 205
  \item \ml{print\_restrict}, \pin{84}
  \item \ml{print\_set}, 84
  \item \ml{print\_state}, \pin{267}
  \item \ml{print\_string}, \pin{73}
  \item \ml{print\_term}, \pin{73}
  \item \ml{print\_theory}, 170
  \item \ml{print\_thm}, \pin{73}
  \item \ml{print\_tok}, \pin{73}
  \item \ml{print\_top\_types}, \pin{84}, 87
  \item \ml{print\_top\_val}, \pin{84}
  \item \ml{print\_type}, \pin{73}
  \item \ml{print\_uncurry}, \pin{84}, 205
  \item \ml{print\_void}, \pin{73}
  \item printing, in \HOL\ logic
    \subitem of function abstractions, 152
    \subitem of hypotheses of theorems, 86, 159
    \subitem of \ml{let}-terms, 153
    \subitem of list expressions, 187
    \subitem of \ml{proof}s, 82
    \subitem of quantification, 205
    \subitem of quotation syntax, 144
    \subitem of theorems, 159
    \subitem of theories, 170
    \subitem of types, 143, 205
    \subitem pretty printing, 205
    \subitem structural depth adjustment in, 75, 214
    \subitem under interface maps, 208
  \item printing, of \ML
    \subitem of abstract-typed values, 20, 50
    \subitem of functions, 9
    \subitem of string quotes, 72
    \subitem user-modified, 86
  \item \ml{prod}, 179
  \item product function operator, in \ML, 56
  \item product types
    \subitem in \HOL\ logic, 179--180
    \subitem in \ML, 40
  \item \ml{prog\_logic88} library, 92
  \item \ml{prompt}, \pin{84}
  \item prompt, in \ML, 7
    \subitem changing of, 85
    \subitem printing of, 84
  \item proof
    \subitem in natural deduction, 117, 158
    \subitem the notion of, in \HOL\ system, 220
  \item \ml{proof}, 259
  \item proof construction, 262
    \subitem as tree search, 257
  \item proof functions (same as justifications, validations), 258
    \subitem \ml{THEN} example of, 276
  \item proof mode, in \HOL\ system, 161, 169
  \item proof steps, as \ML\ function applications, 220, 258, 262
  \item proofs, in \HOL\ logic
    \subitem as generated by derived rules, 220
    \subitem as generated by tactics, 258, 262
    \subitem as \ML\ function applications, 220, 258, 262
  \item \ml{PROVE}, \pin{263}
  \item \ml{prove\_abs\_fn\_one\_one}, \pin{168}
  \item \ml{prove\_abs\_fn\_onto}, \pin{168}
  \item \ml{prove\_cases\_thm}, \pin{203}
  \item \ml{prove\_constructors\_distinct}, \pin{203}
  \item \ml{prove\_constructors\_one\_one}, \pin{203}
  \item \ml{prove\_induction\_thm}, \pin{200}, 202, 203
  \item \ml{prove\_rec\_fn\_exists}, \pin{198}
  \item \ml{prove\_rep\_fn\_one\_one}, \pin{168}
  \item \ml{prove\_rep\_fn\_onto}, \pin{168}
  \item \ml{prove\_thm}, \pin{263}
  \item \ml{PURE\_ASM\_REWRITE\_TAC}, 271
  \item \ml{PURE\_REWRITE\_TAC}, 271

  \indexspace

  \item quantifiers
    \subitem conversions for, 252, 307
    \subitem restricted, 148, 172
  \item \ml{quit}, \pin{76}
  \item quotation, in \HOL\ logic, 144--154
    \subitem of non-primitive terms, 147--154
    \subitem of primitive terms, 146
    \subitem of types, 146
    \subitem parser for, 144, 147
    \subitem typechecker for, 156--157
  \item \ml{quotient} library, 92
  \item quotient types library, 92

  \indexspace

  \item \ml{r}, the subgoal package function, 267
  \item \ml{rand}, 144
  \item \ml{RAND\_CONV}, \pin{247}
  \item \ml{rator}, 144
  \item \ml{RATOR\_CONV}, \pin{247}
  \item \ml{read}, \pin{69}
  \item \ml{rectype}, 19, 24, 48
  \item recursive definitions, in classical logics, 182
  \item recursive definitions, in \HOL\ logic
    \subitem automated for lists, 186--188
    \subitem automated, for numbers, 182--185
    \subitem automated, for recursive types, 197--198
    \subitem automated, for trees, 189--190
  \item recursive types, in \HOL\ logic
    \subitem tools for construction of, 193--195
  \item reduce, 60
  \item reduction, by conversions, 241
  \item \ml{REFL}, 118, 119, \pin{173}, 246
  \item reflexivity, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem \ML\ function for, 173
  \item \ml{remove}, \pin{63}
  \item \ml{remove\_sticky\_type}, \pin{206}
  \item \ml{REP\_}$\ldots$, 195
  \item {\small\verb+rep_+$\ldots$}, 20, 49
  \item \ml{REP\_prod}, 180
  \item \ml{REPEAT}, 272, \pin{277}
  \item \ml{REPEATC}, \pin{242}
  \item repetition
    \subitem of conversions, 242
    \subitem of tactics, 277
  \item \ml{replicate}, \pin{59}
  \item representing types, in \HOL\ logic
    \subitem abstract form of, 130--132
    \subitem pair example of, 179--180
  \item \ml{RES\_ABSTRACT}, 149, 172, 179
  \item \ml{RES\_EXISTS}, 149, 172, 179
  \item \ml{RES\_FORALL}, 149, 172, 179
  \item \ml{RES\_SELECT}, 149, 172, 179
  \item resolution tactics, 271, 277
  \item restrictions, of models, 124
  \item \ml{rev}, \pin{62}
  \item \ml{rev\_assoc}, \pin{62}
  \item \ml{rev\_itlist}, \pin{60}
  \item \ml{REWR\_CONV}, \pin{254}
  \item \ml{REWRITE\_RULE}, 222--223
  \item \ml{REWRITE\_TAC}, 260--261, 269, \pin{270}
  \item rewriting
    \subitem as based on conversions, 254--255
    \subitem importance of, in goal directed proof, 260--261
    \subitem list of tactics for, 255
    \subitem main tactic for, 260--261, 270--271, 277
    \subitem rules for, 222--223
    \subitem use of \ml{DEPTH\_CONV} in, 254
  \item \ml{rhs}, 144
  \item \ml{RIGHT\_BETA}, \pin{234}
  \item \ml{RIGHT\_LIST\_BETA}, \pin{235}
  \item root directory, of \HOL\ system, 89
  \item \ml{rotate}, \pin{266}
  \item rotation, in subgoal package, 264, 266
  \item rules in \HOL\ logic, some not properly derived, 224--225
  \item rules of inference, \see{inference rules}{289}

  \indexspace

  \item \ml{S}, constant in \HOL\ logic, 188
  \item \ml{S}, the constant in \ML, \pin{55}
  \item \ml{S\_DEF}, 188
  \item \ml{S\_THM}, 189
  \item satisfaction of sequents, by model, 116
  \item \ml{save}, \pin{76}
  \item \ml{save\_thm}, \pin{163}
  \item \ml{save\_top\_thm}, \pin{266}
  \item saving theorems, 163
  \item scope
    \subitem in \ML\ abstract types, 49
    \subitem of bindings, 31
  \item search path
    \subitem for \HOL\ system, 70--71, 89
    \subitem for help system, 88
    \subitem for libraries, 90
  \item \ml{search\_path}, \pin{70}
  \item security, in goal directed proof, 259--260
  \item \ml{SELECT\_AX}, 171
    \subitem abstract form of, 123
  \item \ml{SELECT\_ELIM}, \pin{233}
  \item \ml{SELECT\_INTRO}, \pin{232}
  \item selective sequencing tactical, 276
  \item selectors, in \HOL\ logic, 180
  \item sequences, in \ML, 38
  \item sequencing
    \subitem of conversions, 241
    \subitem of \ML\ expressions, 11, 26, 38, 45
    \subitem of tactics, 262, 274--276
  \item sequents
    \subitem in natural deduction, 116, 158
    \subitem representation of, in \HOL\ logic, 158
  \item sessions, with \HOL\ system, 160
  \item set theory (of predicates) library, 92
  \item set theory libraries, 92, 299
  \item set theory notation, 154, 297
  \item \ml{set\_equal}, \pin{65}
  \item \ml{set\_fail}, \pin{67}
  \item \ml{set\_fail\_prefix}, \pin{67}
  \item \ml{set\_flag}, \pin{85}
  \item \ml{set\_goal}, \pin{265}
  \item \ml{set\_help}, \pin{88}, 294
  \item \ml{set\_help\_search\_path}, \pin{88}, 294
  \item \ml{SET\_INDUCT\_TAC}, 300
  \item \ml{set\_interface\_map}, \pin{207}
  \item \ml{set\_lambda}, \pin{211}
  \item \ml{set\_library\_search\_path}, \pin{90}
  \item \ml{set\_margin}, \pin{74}
  \item \ml{set\_pretty\_mode}, \pin{75}
  \item \ml{set\_prompt}, \pin{85}
  \item \ml{set\_search\_path}, \pin{70}
  \item \ml{SET\_SPEC\_CONV}, 300
  \item \ml{set\_state}, \pin{267}
  \item \ml{set\_sticky\_type}, \pin{206}
  \item \ml{set\_string\_escape}, \pin{29}, 302
  \item \ml{set\_thm\_count}, \pin{215}
  \item \ml{set\_turnstile}, \pin{211}
  \item \ml{setify}, \pin{65}
  \item \ml{sets} library, 92
  \item sets, as \ML\ lists, 64
  \item \ml{show\_types}, \pin{84}, 205
  \item side effects, in \ML, 31, 35, 36
  \item side effects, in subgoal package, 265
  \item signatures, of \HOL\ logic
    \subitem formal semantics of, 109
    \subitem of \HOL\ theories, 120
    \subitem standard, 113
  \item simple bindings, in \ML, 33
  \item Skolemization, 251, 306
  \item \ml{snd}, \pin{51}
  \item \ml{SND}, the axiom in \HOL\ logic, 180
  \item \ml{SND}, the constant in \HOL\ logic, 179
  \item \ml{SND\_DEF}, 180
  \item solving, of goals, 258
  \item soundness
    \subitem of \HOL\ deductive system, 119
    \subitem of \HOL\ logic, 212
  \item spaces
    \subitem in \ML\ expressions, 26
    \subitem in \ML\ strings, 29
  \item \ml{SPEC}, 225, \pin{229}
  \item special symbols, in \ML, 27--28
  \item \ml{special\_symbols}, \pin{28}, \pin{141}
  \item specialization rule, in \HOL\ logic, 229
  \item specialization tactic, 268
  \item specification of constants, in \HOL\ logic, 165--172
  \item \ml{split}, \pin{64}, 274
  \item stack, of assumptions, 278
  \item stacks, in subgoal package, 264
  \item standard models, of \HOL\ logic, 113
  \item standard signatures, of \HOL\ logic, 113
  \item standard theory, 123
  \item \ml{sticky}, \pin{84}, 205
  \item sticky types, in \HOL\ logic, 84, 206--207
  \item \ml{sticky\_list}, \pin{207}
  \item stores, 31, 36
  \item strategies, for proof, 257
  \item \ml{string}, 40
  \item \ml{string} library, 92
  \item \ml{string\_of\_int}, \pin{52}
  \item strings, in \ML, 29
    \subitem as input to \HOL\ type definition package, 194
    \subitem changing the escape, 29
    \subitem for input-output, 69
    \subitem processing functions for, 65--66
    \subitem to identify failures, 15, 37
  \item \ml{STRIP\_TAC}, \pin{269}
  \item strong validity, of tactics, 259
  \item structural induction, in \HOL\ logic, \see{induction rule}{289}
  \item \ml{SUB}, 186
  \item \ml{SUB\_CONV}, \pin{247}
  \item subgoal package
    \subitem as \HOL\ interface, 264
    \subitem flags for, 267
    \subitem functions of, 265--267
  \item subgoal tree
    \subitem in proof construction, 264, 277
    \subitem in subgoal package, 264
  \item \ml{subgoals}, 259
  \item \ml{SUBS}, 225
  \item \ml{SUBS\_OCCS}, 225
  \item \ml{SUBST}, 118, 119, 174
  \item \ml{SUBST1\_TAC}, \pin{279}
  \item \ml{SUBST\_CONV}, 225
  \item \ml{SUBST\_TAC}, \pin{269}
  \item substitution rule, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem formal semantics of, 111, 112
    \subitem implementation of, 119
    \subitem \ML\ function for, 174
  \item substitution, tactic for, 269
  \item \ml{subtract}, \pin{64}
  \item successive application
    \subitem conversion operator for, 242
    \subitem tactical for, 276
  \item \ml{sum}, 191
  \item \ml{SUM}, the constant in \HOL\ logic, 188
  \item \ml{SUM}, the theorem in \HOL\ logic, 188
  \item \ml{sum\_Axiom}, 191
  \item \ml{sum\_axiom}, 191
  \item \ml{SYM}, 225, \pin{226}
  \item symbols in \HOL\ logic, changeable, 211--212
  \item symmetry of equality rule, in \HOL\ logic, 226
  \item syntax blocks, 88--89, 301--302
  \item syntax of \ML
    \subitem explanation of, 23
    \subitem short form, 32
  \item \ml{system}, \pin{80}

  \indexspace

  \item \ml{T}, 178
    \subitem abstract form of, 121, 126
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem rules of inference for, 228--230
  \item \ml{T\_DEF}, 171
  \item tab
    \subitem in \ML\ expressions, 27
    \subitem in \ML\ strings, 29
  \item \ml{TAC\_PROOF}, \pin{263}
  \item \ml{tactic}, 259
  \item tacticals, 262, 273--277
    \subitem for alternation, 273
    \subitem for repetition, 277
    \subitem for sequencing, 274--276
    \subitem for successive application, 276
    \subitem list of some, 273--277
    \subitem purpose of, 273, 278, 285
  \item tactics
    \subitem alternation of, 273
    \subitem as documentation of proofs, 257, 285
    \subitem assumption transforming, 277
    \subitem compound, 262, 273
    \subitem debugging of, 263
    \subitem definition of new, 262
    \subitem for manipulating assumptions, 277--288
    \subitem identity for, 272
    \subitem indirect implementation of, 262, 288
    \subitem list of some, 267--273
    \subitem \ML\ type of, 259
    \subitem purpose of, 257--258
    \subitem repetition of, 277
    \subitem sequencing of, 262, 274--276
    \subitem tacticals for, 273--277
    \subitem term transforming, 277
  \item \ml{taut} library, 92
  \item tautologies, in rewriting tactic, 261, 270
  \item tautology checker library, 92
  \item term component, of goal, 258
  \item term constructors, in \HOL\ logic, 143, 146--148
  \item term destructors, in \HOL\ logic, 143
  \item term substitution, in \HOL\ logic, \see{substitution rule}{289}
  \item term-in-context, 108
  \item termination, of \HOL\ sessions, 76
  \item terminator, of \ML\ expressions, 7
  \item terms, in \HOL\ logic
    \subitem antiquotation, 156
    \subitem as logical formulas, 113, 158
    \subitem conditional, 151
    \subitem constructors for, 143, 146--148
    \subitem function abstraction, 146, 152
    \subitem input of, 144
    \subitem \ml{let}-, 153
    \subitem non-primitive, 147
    \subitem pair, 152--153
    \subitem primitive, 146
    \subitem syntax of, 146--154
  \item \ml{THEN}, 262, 272, \pin{274}, 279
    \subitem \ML\ implementation of, 274--276
  \item \ml{THENC}, \pin{241}, 246
  \item \ml{THENL}, 268, 272, 276
  \item \ml{theorem}, \pin{170}
  \item theorem continuations, 278
    \subitem use of, in derivation of induction tactics, 201--203
  \item theorem notation, in \HOL\ logic, 159
  \item \ml{theorems}, \pin{169}
  \item theorems, in \HOL\ logic
    \subitem abstract form of, 120
  \item theorems, in \HOL\ logic
    \subitem as inference rules, 224
    \subitem as rewrite rules, 254
    \subitem destructors for, 158
    \subitem equational, 222, 240
    \subitem rules inexpressible as, 224, 240
    \subitem saving of, 163
  \item theorems, in natural deduction, 158
  \item theorems, printing of, 72
  \item theories, in \HOL\ logic
    \subitem abstract form of, 115, 120
    \subitem caching of, 213
    \subitem creation of, 161--163
    \subitem directory of built-in, 70
    \subitem extension of, 163--167
    \subitem functions for accessing, 169--170
    \subitem hierarchies of, 160, 169, 177
    \subitem naming of, 160
    \subitem paging of, 213
    \subitem representation of, 160--161
  \item theory caching, 213
  \item theory files, 160
    \subitem pretty printing of, 84, 205
  \item theory segments, 160
  \item \ml{theory\_pp}, \pin{84}, 205
  \item \ml{thm}, 158, 173, 219
  \item \ml{thm\_count}, \pin{215}
  \item \ml{thm\_tactic}, 278
  \item \ml{timer}, \pin{215}
  \item \ml{timing}, \pin{84}, 205
  \item timing of \HOL\ evaluations, 215
  \item \ml{tl}, 12, 13, \pin{51}
  \item \ml{TL}, the constant in \HOL\ logic, 186
  \item \ml{TL}, the definition in \HOL\ logic, 188
  \item top level terminator, in \ML, 7
  \item top level, of \ML, 7
    \subitem abstract type expressions at, 50
    \subitem customization of, 85
    \subitem declarations at, 31, 42
    \subitem expressions at, 42
    \subitem printing at, 84
  \item \ml{TOP\_DEPTH\_CONV}, \pin{244}, 248
  \item \ml{top\_goal}, \pin{266}
  \item \ml{top\_print}, 86
  \item \ml{top\_thm}, \pin{266}
  \item \ml{TRANS}, 225, \pin{226}
  \item transitivity of equality rule, in \HOL\ logic, 226
  \item tree of subgoals, in proof construction, 264, 277
  \item \ml{tree}, the \HOL\ theory, 189
  \item \ml{tree}, the \HOL\ type, 189
  \item \ml{tree\_Axiom}, 190
  \item \ml{tree\_Induct}, 190
  \item \ml{trs} library, 92
  \item \ml{true} in \ML, 29, 43
  \item truth values, in \HOL\ logic, 142, 178
    \subitem abstract form of, 114, 121, 126
    \subitem constants for, 171
    \subitem definition of, 171
  \item truth values, in \ML, 29
  \item truth, in \HOL\ logic, \see{\ml{T}}{289}
  \item \ml{TRY\_CONV}, \pin{246}
  \item \ml{tryfind}, \pin{61}
  \item \ml{tty\_read}, \pin{70}
  \item \ml{tty\_write}, \pin{70}
  \item turnstile notation, 117, 158--159
  \item $\ldots$\ml{\_TY\_DEF}, 167, 195
  \item \ml{TY\_DEF\_THM}, 191
  \item \ml{tydefs}, 191
  \item \ml{type}, 17--19, 24, 48
  \item type abbreviations
    \subitem in \HOL\ logic, 176
    \subitem in \ML, 17, 40, 47
  \item type checker, for \HOL\ logic {\it vs} \ML, 146
  \item type checking, in \HOL\ logic
    \subitem antiquotation in, 156
    \subitem of quotation syntax, 144--147
    \subitem special forms in, 147--154
    \subitem sticky types in, 206--207
    \subitem user programmed, 157, 302
    \subitem verbose errors in, 205
  \item type checking, in \ML, 32, 42--45
    \subitem inference involved in, 14, 42--43
    \subitem reasons behind algorithm for, 45--47
    \subitem reasons for, 39
  \item type constants, in \HOL\ logic, 104, 142
  \item type constraint
    \subitem in \HOL\ logic, 102, 142, 145--146
    \subitem in \ML, 7, 24, 25, 42, 44
  \item type constructors
    \subitem in \HOL\ logic, 142, 146
    \subitem in \ML, 20--22, 40--41, 48--50
  \item type context, 105
  \item type definition extension, in \HOL\ logic, 192--195
    \subitem \ML\ function for, 166--167
  \item type definition package, in \HOL\ system, 192--204
    \subitem input to, 194
    \subitem output of, 194--195
    \subitem use of, in case definition, 199
    \subitem use of, in curried infix definition, 200
    \subitem use of, in partial definition, 199
    \subitem use of, in recursive function definition, 197--198
    \subitem use of, in recursive type definition, 193--195
    \subitem use of, to build induction tools, 200--203
    \subitem use of, to build number theory, 196
  \item type definitions, in \HOL\ logic, 166--167
    \subitem abstract structure of, 131
    \subitem autoloading of, 213
    \subitem automated, \see{type definition package}{289}
    \subitem defining bijections for, 167--168
    \subitem introduction of, 166
    \subitem primitive recursive, 182--185
    \subitem properties of bijections for, 168--169
  \item type destructors, in \HOL\ logic, 142
  \item type instantiation, in \HOL\ logic
    \subitem abstract form of, 118
    \subitem in rewriting rule, 222
    \subitem \ML\ function for, 175
  \item type operators, in \HOL\ logic
    \subitem associativity of, 104
    \subitem declaration, 162
    \subitem definitional axioms for, 166
    \subitem for pairs, 179
  \item type operators, in \ML, \see{type constructors}{289}
  \item type specification, 133
  \item type structure, in \HOL\ logic, 104
  \item type structures, of \HOL\ theories, 120
  \item type substitution, in \HOL\ logic
    \subitem formal semantics of, 111
  \item type variables, in \HOL\ logic, 104
    \subitem abstract form of, 103, 113
    \subitem constructor for, 142, 146
    \subitem destructors for, 142
    \subitem differences from classical, 170
    \subitem names of, 140
  \item type variables, in \ML, 14, 24--25, 34, 35, 43
  \item type-in-context, 105
  \item \ml{type\_abbrevs}, \pin{176}
  \item \ml{TYPE\_DEFINITION}, 167, 179
  \item \ml{type\_error}, \pin{84}, 205
  \item \ml{type\_of}, \pin{144}
  \item \ml{types}, \pin{169}
  \item types, in \HOL\ logic, 142
    \subitem  dependent, 295
    \subitem abbreviation of, 176
    \subitem constructors for, 142, 146
    \subitem default, 205--207
    \subitem dependent, 148
    \subitem destructors for, 142
    \subitem determination of, 144
    \subitem explicit printing of, 206
    \subitem generic, 206
    \subitem instantiation of, 106, 112, 175
    \subitem polymorphic, 105, 106
    \subitem printing of, 205
    \subitem sticky, 206--207
    \subitem tools for construction of, 186, 193, 197
  \item types, in \ML
    \subitem abbreviation of, 17, 24, 40, 47
    \subitem abstract, 19--20, 24, 40, 49--50
    \subitem concrete, 17--19, 24, 40, 48
    \subitem printing of, 84, 87
    \subitem printing of currently defined, 82

  \indexspace

  \item \ml{UNCURRY}, 152--153, 179
  \item \ml{uncurry}, \pin{57}
  \item \ml{UNDISCH}, 221, \pin{226}
  \item \ml{undo\_autoload}, \pin{77}, \pin{213}
  \item \ml{unhide\_constant}, \pin{212}
  \item \ml{union}, \pin{64}
  \item universal quantifier, in \HOL\ logic, 178
    \subitem abbreviation for multiple, 121, 148
    \subitem abstract form of, 114, 121, 126
    \subitem defined in terms of primitives, 171
    \subitem definitional axiom for, 171
    \subitem formal semantics of, 122
    \subitem in four primitive axioms, 171
    \subitem inference rules for, 230, 232
    \subitem syntax of, 147
    \subitem tactics for, 268
  \item universe, in semantics of \HOL\ logic, 101
  \item \ml{unlink}, \pin{81}
  \item \ml{unwind} library, 92
  \item unwinding rule library, 92

  \indexspace

  \item validations, 258
  \item validity, of tactics, 259--260, 263
  \item values, of \ML\ variables, 31
  \item Van Tassel, J., 3
  \item variables, in \HOL\ logic
    \subitem abstract form of, 107, 108
    \subitem constructor for, 143, 146
    \subitem destructor for, 143
    \subitem formal semantics of, 110
    \subitem multiple bound, 148
    \subitem names of, 139--141
    \subitem syntax of, 146
    \subitem with constant names, 189, 212
    \subitem with same names, 108
  \item variables, in \ML, 31
    \subitem assignable, 8, 31, 36, 47
    \subitem evaluation of, 35
    \subitem in expression evaluation, 34
    \subitem loading of predefined, 77
    \subitem ordinary, 35
    \subitem syntax of, 24--25
    \subitem type checking of, 43
  \item \ml{version}, \pin{81}
  \item version number, of \HOL\ system, 81
  \item \ml{void}, 37, 40, 41, 43

  \indexspace

  \item \ml{W}, \pin{56}
  \item Wadsworth, C., 3, 222
  \item well-ordering library, 92
  \item {\small\verb+where+}, 8, 26
  \item {\small\verb+whereabsrectype+}, 26
  \item {\small\verb+whereabstype+}, 26
  \item {\small\verb+whererec+}, 26
  \item {\small\verb+whereref+}, 26
  \item {\small\verb+wheretype+}, 26
  \item while construct, in \ML, 26, 37, 45
  \item {\small\ml{while}$\cdots$\ml{do}$\cdots$}
    \subitem evaluation of, 37
    \subitem syntax of, 26
    \subitem type checking of, 45
  \item wildcard, in \ML, 22, 24, 26, 32, 34, 44
  \item word$n$ library, 92
  \item \ml{words}, \pin{65}
  \item \ml{words2}, \pin{65}
  \item \ml{write}, \pin{69}

  \indexspace

  \item \ml{X\_SKOLEM\_CONV}, \pin{251}, 306

  \indexspace

  \item \ml{Z} notation, 125
  \item Zermelo-Fraenkel set theory, 102
  \item \ml{ZFC}, 102

\end{theindex}
