3 \item {\tt !!} symbol, 25
4 \subitem in main goal, 46
5 \item {\tt\%} symbol, 25
6 \item {\tt ::} symbol, 25
7 \item {\tt ==} symbol, 25
8 \item {\tt ==>} symbol, 25
9 \item {\tt =>} symbol, 25
10 \item {\tt =?=} symbol, 25
11 \item {\tt [} symbol, 25
12 \item {\tt [|} symbol, 25
13 \item {\tt ]} symbol, 25
14 \item {\tt\ttlbrace} symbol, 25
15 \item {\tt\ttrbrace} symbol, 25
16 \item {\tt |]} symbol, 25
20 \item {\tt allI} theorem, 37
22 \subitem declaring, 4, \bold{49}
23 \item {\tt asm_simp_tac}, 60
24 \item {\tt assume_tac}, 29, 31, 37, 47
27 \subitem discharge of, 7
28 \subitem lifting over, 14
29 \subitem of main goal, 41
30 \subitem use of, 16, 28
37 \item {\tt back}, 59, 62
39 \subitem Prolog style, 62
47 \item {\tt choplev}, 36, 37, 64
49 \subitem built-in, \bold{25}
50 \item classical reasoner, 39
51 \item {\tt conjunct1} theorem, 27
53 \subitem clashes with variables, 9
54 \subitem declaring, \bold{48}
55 \subitem overloaded, 53
56 \subitem polymorphic, 3
60 \item definitions, 6, \bold{48}
61 \subitem and derived rules, 43--46
62 \item {\tt DEPTH_FIRST}, 64
63 \item destruct-resolution, 22, 30
64 \item {\tt disjE} theorem, 31
65 \item {\tt dres_inst_tac}, 57
66 \item {\tt dresolve_tac}, 30, 32, 38
70 \item eigenvariables, \see{parameters}{8}
71 \item elim-resolution, \bold{20}, 30
73 \subitem polymorphic, 3
74 \item {\tt eres_inst_tac}, 57
75 \item {\tt eresolve_tac}, 30, 32, 38, 47
77 \subitem of deriving rules, 41
78 \subitem of induction, 57, 58
79 \subitem of simplification, 59
80 \subitem of tacticals, 37
81 \subitem of theories, 48, 50--55, 61
82 \subitem propositional, 17, 31, 32
83 \subitem with quantifiers, 18, 33, 35, 37
84 \item {\tt exE} theorem, 38
88 \item {\tt FalseE} theorem, 45
89 \item {\tt fast_tac}, 39
90 \item first-order logic, 1
91 \item flex-flex constraints, 6, 25, \bold{28}
92 \item {\tt flexflex_rule}, 28
93 \item forward proof, 21, 24--30
94 \item {\tt fun} type, 1, 4
95 \item function applications, 1, 8
99 \item {\tt goal}, 30, 41, 46
100 \item {\tt goalw}, 44--46
104 \item {\tt has_fewer_prems}, 64
105 \item higher-order logic, 4
109 \item identifiers, 24
110 \item {\tt impI} theorem, 31, 44
112 \item instantiation, 57--60
114 \subitem object-logics supported, i
116 \subitem release history, i
120 \item $\lambda$-abstractions, 1, 8, 25
121 \item $\lambda$-calculus, 1
123 \item LCF system, 15, 26
124 \item level of a proof, 31
125 \item lifting, \bold{14}
126 \item {\tt logic} class, 3, 6, 25
130 \item major premise, \bold{21}
131 \item {\tt Match} exception, 42
132 \item meta-assumptions
133 \subitem syntax of, 22
134 \item meta-equality, \bold{5}, 25
135 \item meta-implication, \bold{5}, 7, 25
136 \item meta-quantifiers, \bold{5}, 8, 25
137 \item meta-rewriting, 43
138 \item mixfix declarations, 52, 53, 56
140 \item {\tt ML} section, 47
141 \item {\tt mp} theorem, 27
145 \item {\tt Nat} theory, 55
146 \item {\tt nat} type, 1, 3
147 \item {\tt not_def} theorem, 44
148 \item {\tt notE} theorem, \bold{45}, 58
149 \item {\tt notI} theorem, \bold{44}, 58
153 \item {\tt o} type, 1, 4
154 \item {\tt ORELSE}, 37
155 \item overloading, \bold{4}, 53
159 \item parameters, \bold{8}, 33
160 \subitem lifting over, 15
161 \item {\tt Prolog} theory, 61
162 \item Prolog interpreter, \bold{60}
163 \item proof state, 16
165 \subitem commands for, 30
166 \item {\tt PROP} symbol, 26
167 \item {\tt prop} type, 6, 25, 26
169 \item {\tt prthq}, 27, 28
170 \item {\tt prths}, 27
171 \item {\tt Pure} theory, 47
175 \item quantifiers, 5, 8, 33
179 \item {\tt read_instantiate}, 29
180 \item {\tt refl} theorem, 29
181 \item {\tt REPEAT}, 33, 37, 62, 64
182 \item {\tt res_inst_tac}, 57, 60
183 \item reserved words, 24
184 \item resolution, 10, \bold{12}
185 \subitem in backward proof, 15
186 \subitem with instantiation, 57
187 \item {\tt resolve_tac}, 30, 31, 46, 58
188 \item {\tt result}, 30, 42, 46
189 \item {\tt rewrite_goals_tac}, 44
190 \item {\tt rewrite_rule}, 45, 46
193 \item {\tt RS}, 27, 29, 46
194 \item {\tt RSN}, 27, 29
196 \subitem declaring, 48
197 \subitem derived, 13, \bold{22}, 41, 43
198 \subitem destruction, 21
199 \subitem elimination, 21
200 \subitem propositional, 6
201 \subitem quantifier, 8
206 \subitem depth-first, 63
207 \item signatures, \bold{9}
208 \item {\tt simp_tac}, 60
209 \item simplification, 59
210 \item simplification sets, 59
211 \item sort constraints, 25
212 \item sorts, \bold{5}
213 \item {\tt spec} theorem, 28, 36, 37
214 \item {\tt standard}, 27
215 \item substitution, \bold{8}
216 \item {\tt Suc_inject}, 58
217 \item {\tt Suc_neq_0}, 58
219 \subitem of types and terms, 25
223 \item tacticals, \bold{19}, 37
224 \item tactics, \bold{19}
225 \subitem assumption, 29
226 \subitem resolution, 30
227 \item {\tt term} class, 3
229 \subitem syntax of, 1, \bold{25}
231 \subitem basic operations on, \bold{26}
232 \subitem printing of, 27
233 \item theories, \bold{9}
234 \subitem defining, 47--57
235 \item {\tt thm} ML type, 26
236 \item {\tt topthm}, 42
237 \item {\tt Trueprop} constant, 6, 7, 25
238 \item type constraints, 25
239 \item type constructors, 1
240 \item type identifiers, 24
241 \item type synonyms, \bold{51}
243 \subitem declaring, \bold{49}
245 \subitem higher, \bold{5}
246 \subitem polymorphic, \bold{3}
247 \subitem simple, \bold{1}
248 \subitem syntax of, 1, \bold{25}
254 \subitem higher-order, \bold{11}, 58
255 \subitem incompleteness of, 11
256 \item unknowns, 10, 24, 33
257 \subitem function, \bold{11}, 28, 33
258 \item {\tt use_thy}, \bold{47}