145 \item {\tt byev}, \bold{9} |
145 \item {\tt byev}, \bold{9} |
146 |
146 |
147 \indexspace |
147 \indexspace |
148 |
148 |
149 \item {\tt cd}, \bold{3} |
149 \item {\tt cd}, \bold{3} |
150 \item {\tt cert_axm}, \bold{63} |
150 \item {\tt cert_axm}, \bold{64} |
151 \item {\tt CHANGED}, \bold{33} |
151 \item {\tt CHANGED}, \bold{33} |
152 \item {\tt chop}, \bold{11}, 16 |
152 \item {\tt chop}, \bold{11}, 16 |
153 \item {\tt choplev}, \bold{12} |
153 \item {\tt choplev}, \bold{12} |
154 \item {\tt Clarify_step_tac}, \bold{141} |
154 \item {\tt Clarify_step_tac}, \bold{142} |
155 \item {\tt clarify_step_tac}, \bold{138} |
155 \item {\tt clarify_step_tac}, \bold{139} |
156 \item {\tt Clarify_tac}, \bold{141} |
156 \item {\tt Clarify_tac}, \bold{142} |
157 \item {\tt clarify_tac}, \bold{138} |
157 \item {\tt clarify_tac}, \bold{139} |
158 \item {\tt Clarsimp_tac}, \bold{141} |
158 \item {\tt Clarsimp_tac}, \bold{142} |
159 \item {\tt clarsimp_tac}, \bold{139} |
159 \item {\tt clarsimp_tac}, \bold{140} |
160 \item claset |
160 \item claset |
161 \subitem current, 140 |
161 \subitem current, 141 |
162 \item {\tt claset} ML type, 134 |
162 \item {\tt claset} ML type, 135 |
163 \item {\tt ClasimpFun}, 143 |
163 \item {\tt ClasimpFun}, 144 |
164 \item classes |
164 \item classes |
165 \subitem context conditions, 56 |
165 \subitem context conditions, 57 |
166 \item classical reasoner, 129--143 |
166 \item classical reasoner, 130--144 |
167 \subitem setting up, 142 |
167 \subitem setting up, 143 |
168 \subitem tactics, 137 |
168 \subitem tactics, 138 |
169 \item classical sets, 133 |
169 \item classical sets, 134 |
170 \item {\tt ClassicalFun}, 142 |
170 \item {\tt ClassicalFun}, 143 |
171 \item {\tt combination}, \bold{47} |
171 \item {\tt combination}, \bold{48} |
172 \item {\tt commit}, \bold{2} |
172 \item {\tt commit}, \bold{2} |
173 \item {\tt COMP}, \bold{49} |
173 \item {\tt COMP}, \bold{50} |
174 \item {\tt compose}, \bold{49} |
174 \item {\tt compose}, \bold{50} |
175 \item {\tt compose_tac}, \bold{26} |
175 \item {\tt compose_tac}, \bold{26} |
176 \item {\tt concl_of}, \bold{43} |
176 \item {\tt concl_of}, \bold{44} |
177 \item {\tt COND}, \bold{35} |
177 \item {\tt COND}, \bold{35} |
178 \item congruence rules, 110 |
178 \item congruence rules, 111 |
179 \item {\tt Const}, \bold{61}, 87, 97 |
179 \item {\tt Const}, \bold{62}, 88, 98 |
180 \item {\tt Constant}, 84, 97 |
180 \item {\tt Constant}, 85, 98 |
181 \item constants, \bold{61} |
181 \item constants, \bold{62} |
182 \subitem for translations, 74 |
182 \subitem for translations, 75 |
183 \subitem syntactic, 89 |
183 \subitem syntactic, 90 |
184 \item {\tt context}, 104 |
184 \item {\tt context}, 105 |
185 \item {\tt contr_tac}, \bold{141} |
185 \item {\tt contr_tac}, \bold{142} |
186 \item {\tt could_unify}, \bold{28} |
186 \item {\tt could_unify}, \bold{28} |
187 \item {\tt cprems_of}, \bold{43} |
187 \item {\tt cprems_of}, \bold{44} |
188 \item {\tt cprop_of}, \bold{42} |
188 \item {\tt cprop_of}, \bold{43} |
189 \item {\tt CPure} theory, 53 |
189 \item {\tt CPure} theory, 54 |
190 \item {\tt CPure.thy}, \bold{60} |
190 \item {\tt CPure.thy}, \bold{61} |
191 \item {\tt crep_thm}, \bold{43} |
191 \item {\tt crep_thm}, \bold{44} |
192 \item {\tt cterm} ML type, 63 |
192 \item {\tt cterm} ML type, 64 |
193 \item {\tt cterm_instantiate}, \bold{41} |
193 \item {\tt cterm_instantiate}, \bold{42} |
194 \item {\tt cterm_of}, 8, 16, \bold{63} |
194 \item {\tt cterm_of}, 8, 16, \bold{64} |
195 \item {\tt ctyp}, \bold{64} |
195 \item {\tt ctyp}, \bold{65} |
196 \item {\tt ctyp_of}, \bold{65} |
196 \item {\tt ctyp_of}, \bold{66} |
197 \item {\tt cut_facts_tac}, \bold{22}, 102 |
197 \item {\tt cut_facts_tac}, \bold{22}, 103 |
198 \item {\tt cut_inst_tac}, \bold{22} |
198 \item {\tt cut_inst_tac}, \bold{22} |
199 \item {\tt cut_rl} theorem, 24 |
199 \item {\tt cut_rl} theorem, 24 |
200 |
200 |
201 \indexspace |
201 \indexspace |
202 |
202 |
203 \item {\tt datatype}, 106 |
203 \item {\tt datatype}, 107 |
204 \item {\tt Deepen_tac}, \bold{141} |
204 \item {\tt Deepen_tac}, \bold{142} |
205 \item {\tt deepen_tac}, \bold{139} |
205 \item {\tt deepen_tac}, \bold{140} |
206 \item {\tt defer_tac}, \bold{23} |
206 \item {\tt defer_tac}, \bold{23} |
207 \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{56} |
207 \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{57} |
208 \subitem unfolding, 8, 9 |
208 \subitem unfolding, 8, 9 |
209 \item {\tt Delcongs}, \bold{106} |
209 \item {\tt Delcongs}, \bold{107} |
210 \item {\tt delcongs}, \bold{111} |
210 \item {\tt delcongs}, \bold{112} |
211 \item {\tt deleqcongs}, \bold{111} |
211 \item {\tt deleqcongs}, \bold{112} |
212 \item {\tt delete_tmpfiles}, \bold{57} |
212 \item {\tt delete_tmpfiles}, \bold{58} |
213 \item delimiters, \bold{71}, 74, 75, 77 |
213 \item delimiters, \bold{72}, 75, 76, 78 |
214 \item {\tt delloop}, \bold{113} |
214 \item {\tt delloop}, \bold{114} |
215 \item {\tt delrules}, \bold{134} |
215 \item {\tt delrules}, \bold{135} |
216 \item {\tt Delsimprocs}, \bold{106} |
216 \item {\tt Delsimprocs}, \bold{107} |
217 \item {\tt delsimprocs}, \bold{110} |
217 \item {\tt delsimprocs}, \bold{111} |
218 \item {\tt Delsimps}, \bold{106} |
218 \item {\tt Delsimps}, \bold{107} |
219 \item {\tt delsimps}, \bold{109} |
219 \item {\tt delsimps}, \bold{110} |
220 \item {\tt Delsplits}, \bold{106} |
220 \item {\tt Delsplits}, \bold{107} |
221 \item {\tt delSWrapper}, \bold{136} |
221 \item {\tt delSWrapper}, \bold{137} |
222 \item {\tt delWrapper}, \bold{136} |
222 \item {\tt delWrapper}, \bold{137} |
223 \item {\tt dependent_tr'}, 95, \bold{97} |
223 \item {\tt dependent_tr'}, 96, \bold{98} |
224 \item {\tt DEPTH_FIRST}, \bold{34} |
224 \item {\tt DEPTH_FIRST}, \bold{34} |
225 \item {\tt DEPTH_SOLVE}, \bold{34} |
225 \item {\tt DEPTH_SOLVE}, \bold{34} |
226 \item {\tt DEPTH_SOLVE_1}, \bold{34} |
226 \item {\tt DEPTH_SOLVE_1}, \bold{34} |
227 \item {\tt depth_tac}, \bold{139} |
227 \item {\tt depth_tac}, \bold{140} |
228 \item {\tt Deriv.drop}, \bold{51} |
228 \item {\tt Deriv.drop}, \bold{52} |
229 \item {\tt Deriv.linear}, \bold{51} |
229 \item {\tt Deriv.linear}, \bold{52} |
230 \item {\tt Deriv.size}, \bold{51} |
230 \item {\tt Deriv.size}, \bold{52} |
231 \item {\tt Deriv.tree}, \bold{51} |
231 \item {\tt Deriv.tree}, \bold{52} |
232 \item {\tt dest_eq}, \bold{102} |
232 \item {\tt dest_eq}, \bold{103} |
233 \item {\tt dest_imp}, \bold{102} |
233 \item {\tt dest_imp}, \bold{103} |
234 \item {\tt dest_state}, \bold{43} |
234 \item {\tt dest_state}, \bold{44} |
235 \item {\tt dest_Trueprop}, \bold{102} |
235 \item {\tt dest_Trueprop}, \bold{103} |
236 \item destruct-resolution, 20 |
236 \item destruct-resolution, 20 |
237 \item {\tt DETERM}, \bold{35} |
237 \item {\tt DETERM}, \bold{35} |
238 \item discrimination nets, \bold{27} |
238 \item discrimination nets, \bold{27} |
239 \item {\tt distinct_subgoals_tac}, \bold{25} |
239 \item {\tt distinct_subgoals_tac}, \bold{25} |
240 \item {\tt dmatch_tac}, \bold{20} |
240 \item {\tt dmatch_tac}, \bold{20} |
241 \item {\tt domain_type}, \bold{103} |
241 \item {\tt domain_type}, \bold{104} |
242 \item {\tt dres_inst_tac}, \bold{21} |
242 \item {\tt dres_inst_tac}, \bold{21} |
243 \item {\tt dresolve_tac}, \bold{20} |
243 \item {\tt dresolve_tac}, \bold{20} |
244 \item {\tt dtac}, \bold{22} |
244 \item {\tt dtac}, \bold{22} |
245 \item {\tt dummyT}, 87, 88, 98 |
245 \item {\tt dummyT}, 88, 89, 99 |
246 \item duplicate subgoals |
246 \item duplicate subgoals |
247 \subitem removing, 25 |
247 \subitem removing, 25 |
248 |
248 |
249 \indexspace |
249 \indexspace |
250 |
250 |
251 \item elim-resolution, 19 |
251 \item elim-resolution, 19 |
252 \item {\tt ematch_tac}, \bold{20} |
252 \item {\tt ematch_tac}, \bold{20} |
253 \item {\tt empty} constant, 93 |
253 \item {\tt empty} constant, 94 |
254 \item {\tt empty_cs}, \bold{134} |
254 \item {\tt empty_cs}, \bold{135} |
255 \item {\tt empty_ss}, \bold{108} |
255 \item {\tt empty_ss}, \bold{109} |
256 \item {\tt eq_assume_tac}, \bold{20}, 133 |
256 \item {\tt eq_assume_tac}, \bold{20}, 134 |
257 \item {\tt eq_assumption}, \bold{49} |
257 \item {\tt eq_assumption}, \bold{50} |
258 \item {\tt eq_mp_tac}, \bold{141} |
258 \item {\tt eq_mp_tac}, \bold{142} |
259 \item {\tt eq_reflection} theorem, \bold{103}, 124 |
259 \item {\tt eq_reflection} theorem, \bold{104}, 125 |
260 \item {\tt eq_thm}, \bold{35} |
260 \item {\tt eq_thm}, \bold{35} |
261 \item {\tt eq_thy}, \bold{59} |
261 \item {\tt eq_thy}, \bold{60} |
262 \item {\tt equal_elim}, \bold{46} |
262 \item {\tt equal_elim}, \bold{47} |
263 \item {\tt equal_intr}, \bold{46} |
263 \item {\tt equal_intr}, \bold{47} |
264 \item equality, 100--103 |
264 \item equality, 101--104 |
265 \item {\tt eres_inst_tac}, \bold{21} |
265 \item {\tt eres_inst_tac}, \bold{21} |
266 \item {\tt eresolve_tac}, \bold{19} |
266 \item {\tt eresolve_tac}, \bold{19} |
267 \subitem on other than first premise, 42 |
267 \subitem on other than first premise, 43 |
268 \item {\tt ERROR}, 5 |
268 \item {\tt ERROR}, 5 |
269 \item {\tt error}, 5 |
269 \item {\tt error}, 5 |
270 \item error messages, 5 |
270 \item error messages, 5 |
271 \item {\tt eta_contract}, \bold{5}, 91 |
271 \item {\tt eta_contract}, \bold{5}, 92 |
272 \item {\tt etac}, \bold{22} |
272 \item {\tt etac}, \bold{22} |
273 \item {\tt EVERY}, \bold{32} |
273 \item {\tt EVERY}, \bold{32} |
274 \item {\tt EVERY'}, 38 |
274 \item {\tt EVERY'}, 38 |
275 \item {\tt EVERY1}, \bold{38} |
275 \item {\tt EVERY1}, \bold{39} |
276 \item examples |
276 \item examples |
277 \subitem of logic definitions, 81 |
277 \subitem of logic definitions, 82 |
278 \subitem of macros, 93, 94 |
278 \subitem of macros, 94, 95 |
279 \subitem of mixfix declarations, 76 |
279 \subitem of mixfix declarations, 77 |
280 \subitem of simplification, 116 |
280 \subitem of simplification, 117 |
281 \subitem of translations, 97 |
281 \subitem of translations, 98 |
282 \item exceptions |
282 \item exceptions |
283 \subitem printing of, 5 |
283 \subitem printing of, 5 |
284 \item {\tt exit}, \bold{2} |
284 \item {\tt exit}, \bold{2} |
285 \item {\tt extensional}, \bold{47} |
285 \item {\tt extensional}, \bold{48} |
286 |
286 |
287 \indexspace |
287 \indexspace |
288 |
288 |
289 \item {\tt fa}, \bold{14} |
289 \item {\tt fa}, \bold{14} |
290 \item {\tt Fast_tac}, \bold{141} |
290 \item {\tt Fast_tac}, \bold{142} |
291 \item {\tt fast_tac}, \bold{139} |
291 \item {\tt fast_tac}, \bold{140} |
292 \item {\tt fd}, \bold{14} |
292 \item {\tt fd}, \bold{14} |
293 \item {\tt fds}, \bold{14} |
293 \item {\tt fds}, \bold{14} |
294 \item {\tt fe}, \bold{14} |
294 \item {\tt fe}, \bold{14} |
295 \item {\tt fes}, \bold{14} |
295 \item {\tt fes}, \bold{14} |
296 \item files |
296 \item files |
297 \subitem reading, 3, 57 |
297 \subitem reading, 3, 58 |
298 \item {\tt filt_resolve_tac}, \bold{28} |
298 \item {\tt filt_resolve_tac}, \bold{28} |
299 \item {\tt FILTER}, \bold{33} |
299 \item {\tt FILTER}, \bold{33} |
300 \item {\tt filter_goal}, \bold{18} |
300 \item {\tt filter_goal}, \bold{18} |
301 \item {\tt filter_thms}, \bold{28} |
301 \item {\tt filter_thms}, \bold{28} |
302 \item {\tt findE}, \bold{11} |
302 \item {\tt findE}, \bold{11} |
303 \item {\tt findEs}, \bold{11} |
303 \item {\tt findEs}, \bold{11} |
304 \item {\tt findI}, \bold{11} |
304 \item {\tt findI}, \bold{11} |
305 \item {\tt FIRST}, \bold{32} |
305 \item {\tt FIRST}, \bold{32} |
306 \item {\tt FIRST'}, 38 |
306 \item {\tt FIRST'}, 38 |
307 \item {\tt FIRST1}, \bold{38} |
307 \item {\tt FIRST1}, \bold{39} |
308 \item {\tt FIRSTGOAL}, \bold{37} |
308 \item {\tt FIRSTGOAL}, \bold{37} |
309 \item flex-flex constraints, 25, 42, 50 |
309 \item flex-flex constraints, 25, 43, 51 |
310 \item {\tt flexflex_rule}, \bold{50} |
310 \item {\tt flexflex_rule}, \bold{51} |
311 \item {\tt flexflex_tac}, \bold{25} |
311 \item {\tt flexflex_tac}, \bold{25} |
312 \item {\tt FOL_basic_ss}, \bold{127} |
312 \item {\tt FOL_basic_ss}, \bold{128} |
313 \item {\tt FOL_ss}, \bold{127} |
313 \item {\tt FOL_ss}, \bold{128} |
314 \item {\tt fold_goals_tac}, \bold{23} |
314 \item {\tt fold_goals_tac}, \bold{23} |
315 \item {\tt fold_tac}, \bold{23} |
315 \item {\tt fold_tac}, \bold{23} |
316 \item {\tt forall_elim}, \bold{48} |
316 \item {\tt forall_elim}, \bold{49} |
317 \item {\tt forall_elim_list}, \bold{48} |
317 \item {\tt forall_elim_list}, \bold{49} |
318 \item {\tt forall_elim_var}, \bold{48} |
318 \item {\tt forall_elim_var}, \bold{49} |
319 \item {\tt forall_elim_vars}, \bold{48} |
319 \item {\tt forall_elim_vars}, \bold{49} |
320 \item {\tt forall_intr}, \bold{47} |
320 \item {\tt forall_intr}, \bold{48} |
321 \item {\tt forall_intr_frees}, \bold{48} |
321 \item {\tt forall_intr_frees}, \bold{49} |
322 \item {\tt forall_intr_list}, \bold{48} |
322 \item {\tt forall_intr_list}, \bold{49} |
323 \item {\tt force_strip_shyps}, \bold{43} |
323 \item {\tt force_strip_shyps}, \bold{44} |
324 \item {\tt Force_tac}, \bold{141} |
324 \item {\tt Force_tac}, \bold{142} |
325 \item {\tt force_tac}, \bold{138} |
325 \item {\tt force_tac}, \bold{139} |
326 \item {\tt forw_inst_tac}, \bold{21} |
326 \item {\tt forw_inst_tac}, \bold{21} |
327 \item forward proof, 20, 40 |
327 \item forward proof, 20, 41 |
328 \item {\tt forward_tac}, \bold{20} |
328 \item {\tt forward_tac}, \bold{20} |
329 \item {\tt fr}, \bold{14} |
329 \item {\tt fr}, \bold{14} |
330 \item {\tt Free}, \bold{61}, 87 |
330 \item {\tt Free}, \bold{62}, 88 |
331 \item {\tt freezeT}, \bold{48} |
331 \item {\tt freezeT}, \bold{49} |
332 \item {\tt frs}, \bold{14} |
332 \item {\tt frs}, \bold{14} |
333 \item {\tt Full_simp_tac}, \bold{104} |
333 \item {\tt Full_simp_tac}, \bold{105} |
334 \item {\tt full_simp_tac}, \bold{115} |
334 \item {\tt full_simp_tac}, \bold{116} |
335 \item {\tt full_simplify}, 115 |
335 \item {\tt full_simplify}, 116 |
336 \item {\textit {fun}} type, 64 |
336 \item {\textit {fun}} type, 65 |
337 \item function applications, \bold{61} |
337 \item function applications, \bold{62} |
338 |
338 |
339 \indexspace |
339 \indexspace |
340 |
340 |
341 \item {\tt get_axiom}, \bold{10} |
341 \item {\tt get_axiom}, \bold{10} |
342 \item {\tt get_thm}, \bold{10} |
342 \item {\tt get_thm}, \bold{10} |
343 \item {\tt get_thms}, \bold{10} |
343 \item {\tt get_thms}, \bold{10} |
344 \item {\tt getgoal}, \bold{17} |
344 \item {\tt getgoal}, \bold{17} |
345 \item {\tt gethyps}, \bold{18}, 36 |
345 \item {\tt gethyps}, \bold{18}, 37 |
346 \item {\tt Goal}, \bold{8}, 16 |
346 \item {\tt Goal}, \bold{8}, 16 |
347 \item {\tt goal}, \bold{8} |
347 \item {\tt goal}, \bold{8} |
348 \item {\tt goals_limit}, \bold{12} |
348 \item {\tt goals_limit}, \bold{12} |
349 \item {\tt Goalw}, \bold{8} |
349 \item {\tt Goalw}, \bold{8} |
350 \item {\tt goalw}, \bold{8} |
350 \item {\tt goalw}, \bold{8} |
351 \item {\tt goalw_cterm}, \bold{8} |
351 \item {\tt goalw_cterm}, \bold{8} |
352 |
352 |
353 \indexspace |
353 \indexspace |
354 |
354 |
355 \item {\tt has_fewer_prems}, \bold{35} |
355 \item {\tt has_fewer_prems}, \bold{35} |
356 \item higher-order pattern, \bold{109} |
356 \item higher-order pattern, \bold{110} |
357 \item {\tt HOL_basic_ss}, \bold{108} |
357 \item {\tt HOL_basic_ss}, \bold{109} |
358 \item {\tt hyp_subst_tac}, \bold{101} |
358 \item {\tt hyp_subst_tac}, \bold{102} |
359 \item {\tt hyp_subst_tacs}, \bold{143} |
359 \item {\tt hyp_subst_tacs}, \bold{144} |
360 \item {\tt HypsubstFun}, 102, 143 |
360 \item {\tt HypsubstFun}, 103, 144 |
361 |
361 |
362 \indexspace |
362 \indexspace |
363 |
363 |
364 \item {\tt id} nonterminal, \bold{71}, 85, 92 |
364 \item {\tt id} nonterminal, \bold{72}, 86, 93 |
365 \item identifiers, 71 |
365 \item identifiers, 72 |
366 \item {\tt idt} nonterminal, 91 |
366 \item {\tt idt} nonterminal, 92 |
367 \item {\tt idts} nonterminal, \bold{71}, 79 |
367 \item {\tt idts} nonterminal, \bold{72}, 80 |
368 \item {\tt IF_UNSOLVED}, \bold{35} |
368 \item {\tt IF_UNSOLVED}, \bold{35} |
369 \item {\tt iff_reflection} theorem, 124 |
369 \item {\tt iff_reflection} theorem, 125 |
370 \item {\tt IFOL_ss}, \bold{127} |
370 \item {\tt IFOL_ss}, \bold{128} |
371 \item {\tt imp_intr} theorem, \bold{103} |
371 \item {\tt imp_intr} theorem, \bold{104} |
372 \item {\tt implies_elim}, \bold{46} |
372 \item {\tt implies_elim}, \bold{47} |
373 \item {\tt implies_elim_list}, \bold{46} |
373 \item {\tt implies_elim_list}, \bold{47} |
374 \item {\tt implies_intr}, \bold{46} |
374 \item {\tt implies_intr}, \bold{47} |
375 \item {\tt implies_intr_hyps}, \bold{46} |
375 \item {\tt implies_intr_hyps}, \bold{47} |
376 \item {\tt implies_intr_list}, \bold{46} |
376 \item {\tt implies_intr_list}, \bold{47} |
377 \item {\tt incr_boundvars}, \bold{62}, 97 |
377 \item {\tt incr_boundvars}, \bold{63}, 98 |
378 \item {\tt indexname} ML type, 61, 72 |
378 \item {\tt indexname} ML type, 62, 73 |
379 \item infixes, \bold{78} |
379 \item infixes, \bold{79} |
380 \item {\tt insert} constant, 93 |
380 \item {\tt insert} constant, 94 |
381 \item {\tt inst_step_tac}, \bold{140} |
381 \item {\tt inst_step_tac}, \bold{141} |
382 \item {\tt instance} section, 55 |
382 \item {\tt instance} section, 56 |
383 \item {\tt instantiate}, \bold{48} |
383 \item {\tt instantiate}, \bold{49} |
384 \item {\tt instantiate'}, \bold{41}, 48 |
384 \item {\tt instantiate'}, \bold{42}, 49 |
385 \item instantiation, 21, 41, 48 |
385 \item instantiation, 21, 42, 49 |
386 \item {\tt INTLEAVE}, \bold{31}, 33 |
386 \item {\tt INTLEAVE}, \bold{31}, 33 |
387 \item {\tt INTLEAVE'}, 38 |
387 \item {\tt INTLEAVE'}, 38 |
388 \item {\tt invoke_oracle}, \bold{65} |
388 \item {\tt invoke_oracle}, \bold{66} |
389 \item {\tt is} nonterminal, 93 |
389 \item {\tt is} nonterminal, 94 |
390 |
390 |
391 \indexspace |
391 \indexspace |
392 |
392 |
393 \item {\tt joinrules}, \bold{142} |
393 \item {\tt joinrules}, \bold{143} |
394 |
394 |
395 \indexspace |
395 \indexspace |
396 |
396 |
397 \item {\tt keep_derivs}, \bold{51} |
397 \item {\tt keep_derivs}, \bold{52} |
398 |
398 |
399 \indexspace |
399 \indexspace |
400 |
400 |
401 \item $\lambda$-abstractions, 27, \bold{61} |
401 \item $\lambda$-abstractions, 27, \bold{62} |
402 \item $\lambda$-calculus, 45, 47, 71 |
402 \item $\lambda$-calculus, 46, 48, 72 |
403 \item {\tt lessb}, \bold{27} |
403 \item {\tt lessb}, \bold{27} |
404 \item lexer, \bold{71} |
404 \item lexer, \bold{72} |
405 \item {\tt lift_rule}, \bold{50} |
405 \item {\tt lift_rule}, \bold{51} |
406 \item lifting, 50 |
406 \item lifting, 51 |
407 \item {\tt loadpath}, \bold{57} |
407 \item {\tt loadpath}, \bold{58} |
408 \item {\tt logic} class, 71, 76 |
408 \item {\tt logic} class, 72, 77 |
409 \item {\tt logic} nonterminal, \bold{71} |
409 \item {\tt logic} nonterminal, \bold{72} |
410 \item {\tt Logic.auto_rename}, \bold{25} |
410 \item {\tt Logic.auto_rename}, \bold{25} |
411 \item {\tt Logic.set_rename_prefix}, \bold{24} |
411 \item {\tt Logic.set_rename_prefix}, \bold{24} |
412 \item {\tt long_names}, \bold{4} |
412 \item {\tt long_names}, \bold{4} |
413 \item {\tt loose_bnos}, \bold{62}, 98 |
413 \item {\tt loose_bnos}, \bold{63}, 99 |
414 |
414 |
415 \indexspace |
415 \indexspace |
416 |
416 |
417 \item macros, 89--95 |
417 \item macros, 90--96 |
418 \item {\tt make_elim}, \bold{42}, 135 |
418 \item {\tt make_elim}, \bold{43}, 136 |
419 \item {\tt Match} exception, 96 |
419 \item {\tt Match} exception, 97 |
420 \item {\tt match_tac}, \bold{20}, 133 |
420 \item {\tt match_tac}, \bold{20}, 134 |
421 \item {\tt max_pri}, 69, \bold{75} |
421 \item {\tt max_pri}, 70, \bold{76} |
422 \item {\tt merge_ss}, \bold{108} |
422 \item {\tt merge_ss}, \bold{109} |
423 \item {\tt merge_theories}, \bold{60} |
423 \item {\tt merge_theories}, \bold{61} |
424 \item meta-assumptions, 36, 44, 46, 49 |
424 \item meta-assumptions, 36, 45, 47, 50 |
425 \subitem printing of, 4 |
425 \subitem printing of, 4 |
426 \item meta-equality, 45--47 |
426 \item meta-equality, 46--48 |
427 \item meta-implication, 45, 46 |
427 \item meta-implication, 46, 47 |
428 \item meta-quantifiers, 45, 47 |
428 \item meta-quantifiers, 46, 48 |
429 \item meta-rewriting, 8, 14, 15, \bold{23}, |
429 \item meta-rewriting, 8, 14, 15, \bold{23}, |
430 \seealso{tactics, theorems}{144} |
430 \seealso{tactics, theorems}{145} |
431 \subitem in theorems, 41 |
431 \subitem in theorems, 42 |
432 \item meta-rules, \see{meta-rules}{1}, 44--50 |
432 \item meta-rules, \see{meta-rules}{1}, 45--51 |
433 \item {\tt METAHYPS}, 18, \bold{36} |
433 \item {\tt METAHYPS}, 18, \bold{36} |
434 \item mixfix declarations, 54, 74--79 |
434 \item mixfix declarations, 55, 75--80 |
435 \item {\tt mk_atomize}, \bold{126} |
435 \item {\tt mk_atomize}, \bold{127} |
436 \item {\tt mk_simproc}, \bold{122} |
436 \item {\tt mk_simproc}, \bold{123} |
437 \item {\tt ML} section, 56, 96, 98 |
437 \item {\tt ML} section, 57, 97, 99 |
438 \item model checkers, 80 |
438 \item model checkers, 81 |
439 \item {\tt mp} theorem, \bold{142} |
439 \item {\tt mp} theorem, \bold{143} |
440 \item {\tt mp_tac}, \bold{141} |
440 \item {\tt mp_tac}, \bold{142} |
441 \item {\tt MRL}, \bold{40} |
441 \item {\tt MRL}, \bold{41} |
442 \item {\tt MRS}, \bold{40} |
442 \item {\tt MRS}, \bold{41} |
443 |
443 |
444 \indexspace |
444 \indexspace |
445 |
445 |
446 \item name tokens, \bold{71} |
446 \item name tokens, \bold{72} |
447 \item {\tt nat_cancel}, \bold{110} |
447 \item {\tt nat_cancel}, \bold{111} |
448 \item {\tt net_bimatch_tac}, \bold{27} |
448 \item {\tt net_bimatch_tac}, \bold{27} |
449 \item {\tt net_biresolve_tac}, \bold{27} |
449 \item {\tt net_biresolve_tac}, \bold{27} |
450 \item {\tt net_match_tac}, \bold{27} |
450 \item {\tt net_match_tac}, \bold{27} |
451 \item {\tt net_resolve_tac}, \bold{27} |
451 \item {\tt net_resolve_tac}, \bold{27} |
452 \item {\tt no_tac}, \bold{33} |
452 \item {\tt no_tac}, \bold{33} |
453 \item {\tt None}, \bold{29} |
453 \item {\tt None}, \bold{29} |
454 \item {\tt nonterminal} symbols, 54 |
454 \item {\tt nonterminal} symbols, 55 |
455 \item {\tt not_elim} theorem, \bold{142} |
455 \item {\tt not_elim} theorem, \bold{143} |
456 \item {\tt nprems_of}, \bold{43} |
456 \item {\tt nprems_of}, \bold{44} |
457 \item numerals, 71 |
457 \item numerals, 72 |
458 |
458 |
459 \indexspace |
459 \indexspace |
460 |
460 |
461 \item {\textit {o}} type, 81 |
461 \item {\textit {o}} type, 82 |
462 \item {\tt object}, 65 |
462 \item {\tt object}, 66 |
463 \item {\tt op} symbol, 78 |
463 \item {\tt op} symbol, 79 |
464 \item {\tt option} ML type, 29 |
464 \item {\tt option} ML type, 29 |
465 \item oracles, 65--67 |
465 \item oracles, 66--68 |
466 \item {\tt ORELSE}, \bold{31}, 33, 37 |
466 \item {\tt ORELSE}, \bold{31}, 33, 37 |
467 \item {\tt ORELSE'}, 38 |
467 \item {\tt ORELSE'}, 38 |
468 |
468 |
469 \indexspace |
469 \indexspace |
470 |
470 |
471 \item parameters |
471 \item parameters |
472 \subitem removing unused, 25 |
472 \subitem removing unused, 25 |
473 \subitem renaming, 14, 24, 50 |
473 \subitem renaming, 14, 24, 51 |
474 \item {\tt parents_of}, \bold{60} |
474 \item {\tt parents_of}, \bold{61} |
475 \item parse trees, 84 |
475 \item parse trees, 85 |
476 \item {\tt parse_rules}, 91 |
476 \item {\tt parse_rules}, 92 |
477 \item pattern, higher-order, \bold{109} |
477 \item pattern, higher-order, \bold{110} |
478 \item {\tt pause_tac}, \bold{29} |
478 \item {\tt pause_tac}, \bold{29} |
479 \item Poly/{\ML} compiler, 5 |
479 \item Poly/{\ML} compiler, 5 |
480 \item {\tt pop_proof}, \bold{16} |
480 \item {\tt pop_proof}, \bold{16} |
481 \item {\tt pr}, \bold{12} |
481 \item {\tt pr}, \bold{12} |
482 \item {\tt premises}, \bold{8}, 16 |
482 \item {\tt premises}, \bold{8}, 16 |
483 \item {\tt prems_of}, \bold{43} |
483 \item {\tt prems_of}, \bold{44} |
484 \item {\tt prems_of_ss}, \bold{112} |
484 \item {\tt prems_of_ss}, \bold{113} |
485 \item pretty printing, 75, 77--78, 94 |
485 \item pretty printing, 76, 78--79, 95 |
486 \item {\tt Pretty.setdepth}, \bold{4} |
486 \item {\tt Pretty.setdepth}, \bold{4} |
487 \item {\tt Pretty.setmargin}, \bold{4} |
487 \item {\tt Pretty.setmargin}, \bold{4} |
488 \item {\tt PRIMITIVE}, \bold{28} |
488 \item {\tt PRIMITIVE}, \bold{28} |
489 \item {\tt primrec}, 106 |
489 \item {\tt primrec}, 107 |
490 \item {\tt prin}, 6, \bold{17} |
490 \item {\tt prin}, 6, \bold{17} |
491 \item print mode, 54, 98 |
491 \item print mode, 55, 99 |
492 \item print modes, 79--80 |
492 \item print modes, 80--81 |
493 \item {\tt print_cs}, \bold{134} |
493 \item {\tt print_cs}, \bold{135} |
494 \item {\tt print_depth}, \bold{4} |
494 \item {\tt print_depth}, \bold{4} |
495 \item {\tt print_exn}, \bold{6}, 39 |
495 \item {\tt print_exn}, \bold{6}, 40 |
496 \item {\tt print_goals}, \bold{40} |
496 \item {\tt print_goals}, \bold{41} |
497 \item {\tt print_mode}, 79 |
497 \item {\tt print_mode}, 80 |
498 \item {\tt print_modes}, 74 |
498 \item {\tt print_modes}, 75 |
499 \item {\tt print_rules}, 91 |
499 \item {\tt print_rules}, 92 |
500 \item {\tt print_simpset}, \bold{108} |
500 \item {\tt print_simpset}, \bold{109} |
501 \item {\tt print_ss}, \bold{107} |
501 \item {\tt print_ss}, \bold{108} |
502 \item {\tt print_syntax}, \bold{60}, \bold{73} |
502 \item {\tt print_syntax}, \bold{61}, \bold{74} |
503 \item {\tt print_tac}, \bold{29} |
503 \item {\tt print_tac}, \bold{29} |
504 \item {\tt print_theory}, \bold{60} |
504 \item {\tt print_theory}, \bold{61} |
505 \item {\tt print_thm}, \bold{40} |
505 \item {\tt print_thm}, \bold{41} |
506 \item printing control, 3--5 |
506 \item printing control, 3--5 |
507 \item {\tt printyp}, \bold{17} |
507 \item {\tt printyp}, \bold{17} |
508 \item priorities, 68, \bold{75} |
508 \item priorities, 69, \bold{76} |
509 \item priority grammars, 68--69 |
509 \item priority grammars, 69--70 |
510 \item {\tt prlev}, \bold{12} |
510 \item {\tt prlev}, \bold{12} |
511 \item {\tt prlim}, \bold{12} |
511 \item {\tt prlim}, \bold{12} |
512 \item productions, 68, 74, 75 |
512 \item productions, 69, 75, 76 |
513 \subitem copy, \bold{74}, 75, 86 |
513 \subitem copy, \bold{75}, 76, 87 |
514 \item {\tt proof} ML type, 17 |
514 \item {\tt proof} ML type, 17 |
515 \item proof objects, 50--52 |
515 \item proof objects, 51--53 |
516 \item proof state, 7 |
516 \item proof state, 7 |
517 \subitem printing of, 12 |
517 \subitem printing of, 12 |
518 \item {\tt proof_timing}, \bold{13} |
518 \item {\tt proof_timing}, \bold{13} |
519 \item proofs, 7--18 |
519 \item proofs, 7--18 |
520 \subitem inspecting the state, 17 |
520 \subitem inspecting the state, 17 |
521 \subitem managing multiple, 16 |
521 \subitem managing multiple, 16 |
522 \subitem saving and restoring, 17 |
522 \subitem saving and restoring, 17 |
523 \subitem stacking, 16 |
523 \subitem stacking, 16 |
524 \subitem starting, 7 |
524 \subitem starting, 7 |
525 \subitem timing, 13 |
525 \subitem timing, 13 |
526 \item {\tt PROP} symbol, 70 |
526 \item {\tt PROP} symbol, 71 |
527 \item {\textit {prop}} type, 64, 71 |
527 \item {\textit {prop}} type, 65, 72 |
528 \item {\tt prop} nonterminal, \bold{69}, 81 |
528 \item {\tt prop} nonterminal, \bold{70}, 82 |
529 \item {\tt ProtoPure.thy}, \bold{60} |
529 \item {\tt ProtoPure.thy}, \bold{61} |
530 \item {\tt prove_goal}, 13, \bold{15} |
530 \item {\tt prove_goal}, 13, \bold{15} |
531 \item {\tt prove_goalw}, \bold{15} |
531 \item {\tt prove_goalw}, \bold{15} |
532 \item {\tt prove_goalw_cterm}, \bold{15} |
532 \item {\tt prove_goalw_cterm}, \bold{15} |
533 \item {\tt prth}, \bold{39} |
533 \item {\tt prth}, \bold{40} |
534 \item {\tt prthq}, \bold{40} |
534 \item {\tt prthq}, \bold{41} |
535 \item {\tt prths}, \bold{40} |
535 \item {\tt prths}, \bold{41} |
536 \item {\tt prune_params_tac}, \bold{25} |
536 \item {\tt prune_params_tac}, \bold{25} |
537 \item {\tt pttrn} nonterminal, \bold{71} |
537 \item {\tt pttrn} nonterminal, \bold{72} |
538 \item {\tt pttrns} nonterminal, \bold{71} |
538 \item {\tt pttrns} nonterminal, \bold{72} |
539 \item {\tt Pure} theory, 53, 69, 73 |
539 \item {\tt Pure} theory, 54, 70, 74 |
540 \item {\tt Pure.thy}, \bold{60} |
540 \item {\tt Pure.thy}, \bold{61} |
541 \item {\tt push_proof}, \bold{16} |
541 \item {\tt push_proof}, \bold{16} |
542 \item {\tt pwd}, \bold{3} |
542 \item {\tt pwd}, \bold{3} |
543 |
543 |
544 \indexspace |
544 \indexspace |
545 |
545 |
546 \item {\tt qed}, \bold{9}, 11 |
546 \item {\tt qed}, \bold{9}, 11 |
547 \item {\tt qed_goal}, \bold{15} |
547 \item {\tt qed_goal}, \bold{15} |
548 \item {\tt qed_goalw}, \bold{15} |
548 \item {\tt qed_goalw}, \bold{15} |
549 \item quantifiers, 79 |
549 \item quantifiers, 80 |
550 \item {\tt quit}, \bold{2} |
550 \item {\tt quit}, \bold{2} |
551 |
551 |
552 \indexspace |
552 \indexspace |
553 |
553 |
554 \item {\tt read}, \bold{17} |
554 \item {\tt read}, \bold{17} |
555 \item {\tt read_axm}, \bold{63} |
555 \item {\tt read_axm}, \bold{64} |
556 \item {\tt read_cterm}, \bold{63} |
556 \item {\tt read_cterm}, \bold{64} |
557 \item {\tt read_instantiate}, \bold{41} |
557 \item {\tt read_instantiate}, \bold{42} |
558 \item {\tt read_instantiate_sg}, \bold{41} |
558 \item {\tt read_instantiate_sg}, \bold{42} |
559 \item reading |
559 \item reading |
560 \subitem axioms, \see{{\tt assume_ax}}{53} |
560 \subitem axioms, \see{{\tt assume_ax}}{54} |
561 \subitem goals, \see{proofs, starting}{7} |
561 \subitem goals, \see{proofs, starting}{7} |
562 \item {\tt reflexive}, \bold{47} |
562 \item {\tt reflexive}, \bold{48} |
563 \item {\tt ren}, \bold{14} |
563 \item {\tt ren}, \bold{14} |
564 \item {\tt rename_last_tac}, \bold{24} |
564 \item {\tt rename_last_tac}, \bold{24} |
565 \item {\tt rename_params_rule}, \bold{50} |
565 \item {\tt rename_params_rule}, \bold{51} |
566 \item {\tt rename_tac}, \bold{24} |
566 \item {\tt rename_tac}, \bold{24} |
567 \item {\tt rep_cs}, \bold{134} |
567 \item {\tt rep_cs}, \bold{135} |
568 \item {\tt rep_cterm}, \bold{64} |
568 \item {\tt rep_cterm}, \bold{65} |
569 \item {\tt rep_ctyp}, \bold{65} |
569 \item {\tt rep_ctyp}, \bold{66} |
570 \item {\tt rep_ss}, \bold{107} |
570 \item {\tt rep_ss}, \bold{108} |
571 \item {\tt rep_thm}, \bold{43} |
571 \item {\tt rep_thm}, \bold{44} |
572 \item {\tt REPEAT}, \bold{32, 33} |
572 \item {\tt REPEAT}, \bold{32, 33} |
573 \item {\tt REPEAT1}, \bold{32} |
573 \item {\tt REPEAT1}, \bold{32} |
574 \item {\tt REPEAT_DETERM}, \bold{32} |
574 \item {\tt REPEAT_DETERM}, \bold{32} |
575 \item {\tt REPEAT_FIRST}, \bold{37} |
575 \item {\tt REPEAT_FIRST}, \bold{38} |
576 \item {\tt REPEAT_SOME}, \bold{37} |
576 \item {\tt REPEAT_SOME}, \bold{37} |
577 \item {\tt res_inst_tac}, \bold{21}, 25, 26 |
577 \item {\tt res_inst_tac}, \bold{21}, 25, 26 |
578 \item reserved words, 71, 94 |
578 \item reserved words, 72, 95 |
579 \item {\tt reset}, 3 |
579 \item {\tt reset}, 3 |
580 \item resolution, 40, 49 |
580 \item resolution, 41, 50 |
581 \subitem tactics, 19 |
581 \subitem tactics, 19 |
582 \subitem without lifting, 49 |
582 \subitem without lifting, 50 |
583 \item {\tt resolve_tac}, \bold{19}, 133 |
583 \item {\tt resolve_tac}, \bold{19}, 134 |
584 \item {\tt restore_proof}, \bold{17} |
584 \item {\tt restore_proof}, \bold{17} |
585 \item {\tt result}, \bold{9}, 11, 17 |
585 \item {\tt result}, \bold{9}, 11, 17 |
586 \item {\tt rev_mp} theorem, \bold{103} |
586 \item {\tt rev_mp} theorem, \bold{104} |
587 \item rewrite rules, 109 |
587 \item rewrite rules, 110 |
588 \subitem permutative, 119--122 |
588 \subitem permutative, 120--123 |
589 \item {\tt rewrite_goals_rule}, \bold{41} |
589 \item {\tt rewrite_goals_rule}, \bold{42} |
590 \item {\tt rewrite_goals_tac}, \bold{23}, 41 |
590 \item {\tt rewrite_goals_tac}, \bold{23}, 42 |
591 \item {\tt rewrite_rule}, \bold{41} |
591 \item {\tt rewrite_rule}, \bold{42} |
592 \item {\tt rewrite_tac}, 9, \bold{23} |
592 \item {\tt rewrite_tac}, 9, \bold{23} |
593 \item rewriting |
593 \item rewriting |
594 \subitem object-level, \see{simplification}{1} |
594 \subitem object-level, \see{simplification}{1} |
595 \subitem ordered, 120 |
595 \subitem ordered, 121 |
596 \subitem syntactic, 89--95 |
596 \subitem syntactic, 90--96 |
597 \item {\tt rewtac}, \bold{22} |
597 \item {\tt rewtac}, \bold{22} |
598 \item {\tt RL}, \bold{40} |
598 \item {\tt RL}, \bold{41} |
599 \item {\tt RLN}, \bold{40} |
599 \item {\tt RLN}, \bold{41} |
600 \item {\tt rotate_prems}, \bold{42} |
600 \item {\tt rotate_prems}, \bold{43} |
601 \item {\tt rotate_proof}, \bold{16} |
601 \item {\tt rotate_proof}, \bold{16} |
602 \item {\tt rotate_tac}, \bold{25} |
602 \item {\tt rotate_tac}, \bold{25} |
603 \item {\tt RS}, \bold{40} |
603 \item {\tt RS}, \bold{41} |
604 \item {\tt RSN}, \bold{40} |
604 \item {\tt RSN}, \bold{41} |
605 \item {\tt rtac}, \bold{22} |
605 \item {\tt rtac}, \bold{22} |
606 \item {\tt rule_by_tactic}, 25, \bold{42} |
606 \item {\tt rule_by_tactic}, 25, \bold{43} |
607 \item rules |
607 \item rules |
608 \subitem converting destruction to elimination, 42 |
608 \subitem converting destruction to elimination, 43 |
609 |
609 |
610 \indexspace |
610 \indexspace |
611 |
611 |
612 \item {\tt safe_asm_full_simp_tac}, \bold{115} |
612 \item {\tt safe_asm_full_simp_tac}, \bold{116} |
613 \item {\tt Safe_step_tac}, \bold{141} |
613 \item {\tt Safe_step_tac}, \bold{142} |
614 \item {\tt safe_step_tac}, 135, \bold{140} |
614 \item {\tt safe_step_tac}, 136, \bold{141} |
615 \item {\tt Safe_tac}, \bold{141} |
615 \item {\tt Safe_tac}, \bold{142} |
616 \item {\tt safe_tac}, \bold{140} |
616 \item {\tt safe_tac}, \bold{141} |
617 \item {\tt save_proof}, \bold{17} |
617 \item {\tt save_proof}, \bold{17} |
618 \item saving your work, \bold{1} |
618 \item saving your work, \bold{1} |
619 \item search, 31 |
619 \item search, 31 |
620 \subitem tacticals, 33--35 |
620 \subitem tacticals, 33--35 |
621 \item {\tt SELECT_GOAL}, 23, \bold{36} |
621 \item {\tt SELECT_GOAL}, 23, \bold{36} |
622 \item {\tt Seq.seq} ML type, 28 |
622 \item {\tt Seq.seq} ML type, 28 |
623 \item sequences (lazy lists), \bold{29} |
623 \item sequences (lazy lists), \bold{29} |
624 \item sequent calculus, 130 |
624 \item sequent calculus, 131 |
625 \item sessions, 1--6 |
625 \item sessions, 1--6 |
626 \item {\tt set}, 3 |
626 \item {\tt set}, 3 |
627 \item {\tt setloop}, \bold{113} |
627 \item {\tt setloop}, \bold{114} |
628 \item {\tt setmksimps}, 109, \bold{125}, 127 |
628 \item {\tt setmksimps}, 110, \bold{126}, 128 |
629 \item {\tt setSolver}, \bold{112}, 127 |
629 \item {\tt setSolver}, \bold{113}, 128 |
630 \item {\tt setSSolver}, \bold{112}, 127 |
630 \item {\tt setSSolver}, \bold{113}, 128 |
631 \item {\tt setsubgoaler}, \bold{111}, 127 |
631 \item {\tt setsubgoaler}, \bold{112}, 128 |
632 \item {\tt settermless}, \bold{120} |
632 \item {\tt settermless}, \bold{121} |
633 \item {\tt setup} |
633 \item {\tt setup} |
634 \subitem simplifier, 128 |
634 \subitem simplifier, 129 |
635 \subitem theory, 55 |
635 \subitem theory, 56 |
636 \item shortcuts |
636 \item shortcuts |
637 \subitem for \texttt{by} commands, 13 |
637 \subitem for \texttt{by} commands, 13 |
638 \subitem for tactics, 22 |
638 \subitem for tactics, 22 |
639 \item {\tt show_brackets}, \bold{4} |
639 \item {\tt show_brackets}, \bold{4} |
640 \item {\tt show_consts}, \bold{4} |
640 \item {\tt show_consts}, \bold{4} |
641 \item {\tt show_hyps}, \bold{4} |
641 \item {\tt show_hyps}, \bold{4} |
642 \item {\tt show_sorts}, \bold{4}, 88, 96 |
642 \item {\tt show_sorts}, \bold{4}, 89, 97 |
643 \item {\tt show_types}, \bold{4}, 88, 91, 98 |
643 \item {\tt show_types}, \bold{4}, 89, 92, 99 |
644 \item {\tt Sign.certify_term}, \bold{64} |
644 \item {\tt Sign.certify_term}, \bold{65} |
645 \item {\tt Sign.certify_typ}, \bold{65} |
645 \item {\tt Sign.certify_typ}, \bold{66} |
646 \item {\tt Sign.sg} ML type, 53 |
646 \item {\tt Sign.sg} ML type, 54 |
647 \item {\tt Sign.stamp_names_of}, \bold{61} |
647 \item {\tt Sign.stamp_names_of}, \bold{62} |
648 \item {\tt Sign.string_of_term}, \bold{63} |
648 \item {\tt Sign.string_of_term}, \bold{64} |
649 \item {\tt Sign.string_of_typ}, \bold{65} |
649 \item {\tt Sign.string_of_typ}, \bold{66} |
650 \item {\tt sign_of}, 8, 16, \bold{61} |
650 \item {\tt sign_of}, 8, 16, \bold{62} |
651 \item {\tt sign_of_thm}, \bold{43} |
651 \item {\tt sign_of_thm}, \bold{44} |
652 \item signatures, \bold{53}, 61, 63, 65 |
652 \item signatures, \bold{54}, 62, 64, 66 |
653 \item {\tt Simp_tac}, \bold{104} |
653 \item {\tt Simp_tac}, \bold{105} |
654 \item {\tt simp_tac}, \bold{115} |
654 \item {\tt simp_tac}, \bold{116} |
655 \item simplification, 104--128 |
655 \item simplification, 105--129 |
656 \subitem conversions, 115 |
656 \subitem conversions, 116 |
657 \subitem forward rules, 115 |
657 \subitem forward rules, 116 |
658 \subitem from classical reasoner, 136 |
658 \subitem from classical reasoner, 137 |
659 \subitem setting up, 124 |
659 \subitem setting up, 125 |
660 \subitem setting up the splitter, 128 |
660 \subitem setting up the splitter, 129 |
661 \subitem setting up the theory, 128 |
661 \subitem setting up the theory, 129 |
662 \subitem tactics, 114 |
662 \subitem tactics, 115 |
663 \item simplification sets, 107 |
663 \item simplification sets, 108 |
664 \item {\tt Simplifier.asm_full_rewrite}, 115 |
664 \item {\tt Simplifier.asm_full_rewrite}, 116 |
665 \item {\tt Simplifier.asm_rewrite}, 115 |
665 \item {\tt Simplifier.asm_rewrite}, 116 |
666 \item {\tt Simplifier.full_rewrite}, 115 |
666 \item {\tt Simplifier.full_rewrite}, 116 |
667 \item {\tt Simplifier.rewrite}, 115 |
667 \item {\tt Simplifier.rewrite}, 116 |
668 \item {\tt Simplifier.setup}, \bold{128} |
668 \item {\tt Simplifier.setup}, \bold{129} |
669 \item {\tt simplify}, 115 |
669 \item {\tt simplify}, 116 |
670 \item {\tt SIMPSET}, \bold{108} |
670 \item {\tt SIMPSET}, \bold{109} |
671 \item simpset |
671 \item simpset |
672 \subitem current, 104, 108 |
672 \subitem current, 105, 109 |
673 \item {\tt simpset}, \bold{108} |
673 \item {\tt simpset}, \bold{109} |
674 \item {\tt SIMPSET'}, \bold{108} |
674 \item {\tt SIMPSET'}, \bold{109} |
675 \item {\tt simpset_of}, \bold{108} |
675 \item {\tt simpset_of}, \bold{109} |
676 \item {\tt simpset_ref}, \bold{108} |
676 \item {\tt simpset_ref}, \bold{109} |
677 \item {\tt simpset_ref_of}, \bold{108} |
677 \item {\tt simpset_ref_of}, \bold{109} |
678 \item {\tt size_of_thm}, 34, \bold{35}, 142 |
678 \item {\tt size_of_thm}, 34, \bold{35}, 143 |
679 \item {\tt sizef}, \bold{142} |
679 \item {\tt sizef}, \bold{143} |
680 \item {\tt slow_best_tac}, \bold{139} |
680 \item {\tt slow_best_tac}, \bold{140} |
681 \item {\tt slow_step_tac}, 135, \bold{140} |
681 \item {\tt slow_step_tac}, 136, \bold{141} |
682 \item {\tt slow_tac}, \bold{139} |
682 \item {\tt slow_tac}, \bold{140} |
|
683 \item {\tt SOLVE}, \bold{35} |
683 \item {\tt Some}, \bold{29} |
684 \item {\tt Some}, \bold{29} |
684 \item {\tt SOMEGOAL}, \bold{37} |
685 \item {\tt SOMEGOAL}, \bold{37} |
685 \item {\tt sort} nonterminal, \bold{71} |
686 \item {\tt sort} nonterminal, \bold{72} |
686 \item sort constraints, 70 |
687 \item sort constraints, 71 |
687 \item sort hypotheses, 43 |
688 \item sort hypotheses, 44 |
688 \item sorts |
689 \item sorts |
689 \subitem printing of, 4 |
690 \subitem printing of, 4 |
690 \item {\tt ssubst} theorem, \bold{100} |
691 \item {\tt ssubst} theorem, \bold{101} |
691 \item {\tt stac}, \bold{101} |
692 \item {\tt stac}, \bold{102} |
692 \item stamps, \bold{53}, 61 |
693 \item stamps, \bold{54}, 62 |
693 \item {\tt standard}, \bold{42} |
694 \item {\tt standard}, \bold{43} |
694 \item starting up, \bold{1} |
695 \item starting up, \bold{1} |
695 \item {\tt Step_tac}, \bold{141} |
696 \item {\tt Step_tac}, \bold{142} |
696 \item {\tt step_tac}, 135, \bold{140} |
697 \item {\tt step_tac}, 136, \bold{141} |
697 \item {\tt store_thm}, \bold{10} |
698 \item {\tt store_thm}, \bold{10} |
698 \item {\tt string_of_cterm}, \bold{63} |
699 \item {\tt string_of_cterm}, \bold{64} |
699 \item {\tt string_of_ctyp}, \bold{65} |
700 \item {\tt string_of_ctyp}, \bold{66} |
700 \item {\tt string_of_thm}, \bold{40} |
701 \item {\tt string_of_thm}, \bold{41} |
701 \item strings, 71 |
702 \item strings, 72 |
702 \item {\tt SUBGOAL}, \bold{28} |
703 \item {\tt SUBGOAL}, \bold{28} |
703 \item subgoal module, 7--18 |
704 \item subgoal module, 7--18 |
704 \item {\tt subgoal_tac}, \bold{22} |
705 \item {\tt subgoal_tac}, \bold{22} |
705 \item {\tt subgoals_of_brl}, \bold{26} |
706 \item {\tt subgoals_of_brl}, \bold{26} |
706 \item {\tt subgoals_tac}, \bold{23} |
707 \item {\tt subgoals_tac}, \bold{23} |
707 \item {\tt subst} theorem, 100, \bold{103} |
708 \item {\tt subst} theorem, 101, \bold{104} |
708 \item substitution |
709 \item substitution |
709 \subitem rules, 100 |
710 \subitem rules, 101 |
710 \item {\tt subthy}, \bold{59} |
711 \item {\tt subthy}, \bold{60} |
711 \item {\tt swap} theorem, \bold{142} |
712 \item {\tt swap} theorem, \bold{143} |
712 \item {\tt swap_res_tac}, \bold{142} |
713 \item {\tt swap_res_tac}, \bold{143} |
713 \item {\tt swapify}, \bold{142} |
714 \item {\tt swapify}, \bold{143} |
714 \item {\tt sym} theorem, 101, \bold{103} |
715 \item {\tt sym} theorem, 102, \bold{104} |
715 \item {\tt symmetric}, \bold{47} |
716 \item {\tt symmetric}, \bold{48} |
716 \item {\tt syn_of}, \bold{73} |
717 \item {\tt syn_of}, \bold{74} |
717 \item syntax |
718 \item syntax |
718 \subitem Pure, 69--74 |
719 \subitem Pure, 70--75 |
719 \subitem transformations, 84--98 |
720 \subitem transformations, 85--99 |
720 \item {\tt syntax} section, 54 |
721 \item {\tt syntax} section, 55 |
721 \item {\tt Syntax.ast} ML type, 84 |
722 \item {\tt Syntax.ast} ML type, 85 |
722 \item {\tt Syntax.mark_boundT}, 98 |
723 \item {\tt Syntax.mark_boundT}, 99 |
723 \item {\tt Syntax.print_gram}, \bold{73} |
724 \item {\tt Syntax.print_gram}, \bold{74} |
724 \item {\tt Syntax.print_syntax}, \bold{73} |
725 \item {\tt Syntax.print_syntax}, \bold{74} |
725 \item {\tt Syntax.print_trans}, \bold{73} |
726 \item {\tt Syntax.print_trans}, \bold{74} |
726 \item {\tt Syntax.stat_norm_ast}, 93 |
727 \item {\tt Syntax.stat_norm_ast}, 94 |
727 \item {\tt Syntax.syntax} ML type, 73 |
728 \item {\tt Syntax.syntax} ML type, 74 |
728 \item {\tt Syntax.test_read}, 77, 93 |
729 \item {\tt Syntax.test_read}, 78, 94 |
729 \item {\tt Syntax.trace_norm_ast}, 93 |
730 \item {\tt Syntax.trace_norm_ast}, 94 |
730 \item {\tt Syntax.variant_abs'}, 98 |
731 \item {\tt Syntax.variant_abs'}, 99 |
731 |
732 |
732 \indexspace |
733 \indexspace |
733 |
734 |
734 \item {\tt tactic} ML type, 19 |
735 \item {\tt tactic} ML type, 19 |
735 \item tacticals, 31--38 |
736 \item tacticals, 31--39 |
736 \subitem conditional, 35 |
737 \subitem conditional, 35 |
737 \subitem deterministic, 35 |
738 \subitem deterministic, 35 |
738 \subitem for filtering, 33 |
739 \subitem for filtering, 33 |
739 \subitem for restriction to a subgoal, 36 |
740 \subitem for restriction to a subgoal, 36 |
740 \subitem identities for, 32 |
741 \subitem identities for, 32 |
748 \subitem assumption, \bold{20}, 22 |
749 \subitem assumption, \bold{20}, 22 |
749 \subitem commands for applying, 8 |
750 \subitem commands for applying, 8 |
750 \subitem debugging, 17 |
751 \subitem debugging, 17 |
751 \subitem filtering results of, 33 |
752 \subitem filtering results of, 33 |
752 \subitem for composition, 26 |
753 \subitem for composition, 26 |
753 \subitem for contradiction, 141 |
754 \subitem for contradiction, 142 |
754 \subitem for inserting facts, 22 |
755 \subitem for inserting facts, 22 |
755 \subitem for Modus Ponens, 141 |
756 \subitem for Modus Ponens, 142 |
756 \subitem instantiation, 21 |
757 \subitem instantiation, 21 |
757 \subitem matching, 20 |
758 \subitem matching, 20 |
758 \subitem meta-rewriting, 22, \bold{23} |
759 \subitem meta-rewriting, 22, \bold{23} |
759 \subitem primitives for coding, 28 |
760 \subitem primitives for coding, 28 |
760 \subitem resolution, \bold{19}, 22, 26, 27 |
761 \subitem resolution, \bold{19}, 22, 26, 27 |
761 \subitem restricting to a subgoal, 36 |
762 \subitem restricting to a subgoal, 36 |
762 \subitem simplification, 114 |
763 \subitem simplification, 115 |
763 \subitem substitution, 100--103 |
764 \subitem substitution, 101--104 |
764 \subitem tracing, 29 |
765 \subitem tracing, 29 |
765 \item {\tt TERM}, 63 |
766 \item {\tt TERM}, 64 |
766 \item {\tt term} ML type, 61, 87 |
767 \item {\tt term} ML type, 62, 88 |
767 \item terms, \bold{61} |
768 \item terms, \bold{62} |
768 \subitem certified, \bold{63} |
769 \subitem certified, \bold{64} |
769 \subitem made from ASTs, 87 |
770 \subitem made from ASTs, 88 |
770 \subitem printing of, 17, 63 |
771 \subitem printing of, 17, 64 |
771 \subitem reading of, 17 |
772 \subitem reading of, 17 |
772 \item {\tt TFree}, \bold{64} |
773 \item {\tt TFree}, \bold{65} |
773 \item {\tt THEN}, \bold{31}, 33, 37 |
774 \item {\tt THEN}, \bold{31}, 33, 37 |
774 \item {\tt THEN'}, 38 |
775 \item {\tt THEN'}, 38 |
775 \item {\tt THEN_BEST_FIRST}, \bold{34} |
776 \item {\tt THEN_BEST_FIRST}, \bold{34} |
776 \item theorems, 39--52 |
777 \item theorems, 40--53 |
777 \subitem equality of, 35 |
778 \subitem equality of, 35 |
778 \subitem extracting, 10 |
779 \subitem extracting, 10 |
779 \subitem extracting proved, 9 |
780 \subitem extracting proved, 9 |
780 \subitem joining by resolution, 40 |
781 \subitem joining by resolution, 41 |
781 \subitem of pure theory, 24 |
782 \subitem of pure theory, 24 |
782 \subitem printing of, 39 |
783 \subitem printing of, 40 |
783 \subitem retrieving, 11 |
784 \subitem retrieving, 11 |
784 \subitem size of, 35 |
785 \subitem size of, 35 |
785 \subitem standardizing, 42 |
786 \subitem standardizing, 43 |
786 \subitem storing, 10 |
787 \subitem storing, 10 |
787 \subitem taking apart, 42 |
788 \subitem taking apart, 43 |
788 \item theories, 53--67 |
789 \item theories, 54--68 |
789 \subitem axioms of, 10 |
790 \subitem axioms of, 10 |
790 \subitem constructing, \bold{60} |
791 \subitem constructing, \bold{61} |
791 \subitem inspecting, \bold{60} |
792 \subitem inspecting, \bold{61} |
792 \subitem loading, 57 |
793 \subitem loading, 58 |
793 \subitem parent, \bold{53} |
794 \subitem parent, \bold{54} |
794 \subitem pseudo, \bold{58} |
795 \subitem pseudo, \bold{59} |
795 \subitem reloading, \bold{58} |
796 \subitem reloading, \bold{59} |
796 \subitem removing, \bold{58} |
797 \subitem removing, \bold{59} |
797 \subitem theorems of, 10 |
798 \subitem theorems of, 10 |
798 \item {\tt THEORY} exception, 10, 53 |
799 \item {\tt THEORY} exception, 10, 54 |
799 \item {\tt theory} ML type, 53 |
800 \item {\tt theory} ML type, 54 |
800 \item {\tt Theory.add_oracle}, \bold{65} |
801 \item {\tt Theory.add_oracle}, \bold{66} |
801 \item {\tt theory_of_thm}, \bold{43} |
802 \item {\tt theory_of_thm}, \bold{44} |
802 \item {\tt thin_refl} theorem, \bold{103} |
803 \item {\tt thin_refl} theorem, \bold{104} |
803 \item {\tt thin_tac}, \bold{25} |
804 \item {\tt thin_tac}, \bold{25} |
804 \item {\tt THM} exception, 39, 40, 44, 49 |
805 \item {\tt THM} exception, 40, 41, 45, 50 |
805 \item {\tt thm}, \bold{10} |
806 \item {\tt thm}, \bold{10} |
806 \item {\tt thm} ML type, 39 |
807 \item {\tt thm} ML type, 40 |
807 \item {\tt thms}, \bold{10} |
808 \item {\tt thms}, \bold{10} |
808 \item {\tt thms_containing}, \bold{11} |
809 \item {\tt thms_containing}, \bold{11} |
809 \item {\tt thms_of}, \bold{10} |
810 \item {\tt thms_of}, \bold{10} |
810 \item {\tt tid} nonterminal, \bold{71}, 85, 92 |
811 \item {\tt tid} nonterminal, \bold{72}, 86, 93 |
811 \item {\tt time_use}, \bold{3} |
812 \item {\tt time_use}, \bold{3} |
812 \item {\tt time_use_thy}, \bold{57} |
813 \item {\tt time_use_thy}, \bold{58} |
813 \item timing statistics, 13 |
814 \item timing statistics, 13 |
814 \item {\tt toggle}, 3 |
815 \item {\tt toggle}, 3 |
815 \item token class, 98 |
816 \item token class, 99 |
816 \item token translations, 98--99 |
817 \item token translations, 99--100 |
817 \item token_translation, 99 |
818 \item token_translation, 100 |
818 \item {\tt token_translation}, 99 |
819 \item {\tt token_translation}, 100 |
819 \item {\tt topthm}, \bold{17} |
820 \item {\tt topthm}, \bold{17} |
820 \item {\tt tpairs_of}, \bold{43} |
821 \item {\tt tpairs_of}, \bold{44} |
821 \item {\tt trace_BEST_FIRST}, \bold{34} |
822 \item {\tt trace_BEST_FIRST}, \bold{34} |
822 \item {\tt trace_DEPTH_FIRST}, \bold{34} |
823 \item {\tt trace_DEPTH_FIRST}, \bold{34} |
823 \item {\tt trace_goalno_tac}, \bold{37} |
824 \item {\tt trace_goalno_tac}, \bold{38} |
824 \item {\tt trace_REPEAT}, \bold{32} |
825 \item {\tt trace_REPEAT}, \bold{32} |
825 \item {\tt trace_simp}, \bold{105}, 117 |
826 \item {\tt trace_simp}, \bold{106}, 118 |
826 \item tracing |
827 \item tracing |
827 \subitem of classical prover, 138 |
828 \subitem of classical prover, 139 |
828 \subitem of macros, 93 |
829 \subitem of macros, 94 |
829 \subitem of searching tacticals, 34 |
830 \subitem of searching tacticals, 34 |
830 \subitem of simplification, 106, 117--118 |
831 \subitem of simplification, 107, 118--119 |
831 \subitem of tactics, 29 |
832 \subitem of tactics, 29 |
832 \subitem of unification, 44 |
833 \subitem of unification, 45 |
833 \item {\tt transfer}, \bold{59} |
834 \item {\tt transfer}, \bold{60} |
834 \item {\tt transfer_sg}, \bold{59} |
835 \item {\tt transfer_sg}, \bold{60} |
835 \item {\tt transitive}, \bold{47} |
836 \item {\tt transitive}, \bold{48} |
836 \item translations, 95--98 |
837 \item translations, 96--99 |
837 \subitem parse, 79, 87 |
838 \subitem parse, 80, 88 |
838 \subitem parse AST, \bold{85}, 86 |
839 \subitem parse AST, \bold{86}, 87 |
839 \subitem print, 79 |
840 \subitem print, 80 |
840 \subitem print AST, \bold{88} |
841 \subitem print AST, \bold{89} |
841 \item {\tt translations} section, 90 |
842 \item {\tt translations} section, 91 |
842 \item {\tt trivial}, \bold{50} |
843 \item {\tt trivial}, \bold{51} |
843 \item {\tt Trueprop} constant, 81 |
844 \item {\tt Trueprop} constant, 82 |
844 \item {\tt TRY}, \bold{32, 33} |
845 \item {\tt TRY}, \bold{32, 33} |
845 \item {\tt TRYALL}, \bold{37} |
846 \item {\tt TRYALL}, \bold{37} |
846 \item {\tt TVar}, \bold{64} |
847 \item {\tt TVar}, \bold{65} |
847 \item {\tt tvar} nonterminal, \bold{71, 72}, 85, 92 |
848 \item {\tt tvar} nonterminal, \bold{72, 73}, 86, 93 |
848 \item {\tt typ} ML type, 64 |
849 \item {\tt typ} ML type, 65 |
849 \item {\tt Type}, \bold{64} |
850 \item {\tt Type}, \bold{65} |
850 \item {\textit {type}} type, 76 |
851 \item {\textit {type}} type, 77 |
851 \item {\tt type} nonterminal, \bold{71} |
852 \item {\tt type} nonterminal, \bold{72} |
852 \item type constraints, 71, 79, 88 |
853 \item type constraints, 72, 80, 89 |
853 \item type constructors, \bold{64} |
854 \item type constructors, \bold{65} |
854 \item type identifiers, 71 |
855 \item type identifiers, 72 |
855 \item type synonyms, \bold{54} |
856 \item type synonyms, \bold{55} |
856 \item type unknowns, \bold{64}, 71 |
857 \item type unknowns, \bold{65}, 72 |
857 \subitem freezing/thawing of, 48 |
858 \subitem freezing/thawing of, 49 |
858 \item type variables, \bold{64} |
859 \item type variables, \bold{65} |
859 \item types, \bold{64} |
860 \item types, \bold{65} |
860 \subitem certified, \bold{64} |
861 \subitem certified, \bold{65} |
861 \subitem printing of, 4, 17, 64 |
862 \subitem printing of, 4, 17, 65 |
862 |
863 |
863 \indexspace |
864 \indexspace |
864 |
865 |
865 \item {\tt undo}, 7, \bold{12}, 16 |
866 \item {\tt undo}, 7, \bold{12}, 16 |
866 \item unknowns, \bold{61}, 71 |
867 \item unknowns, \bold{62}, 72 |
867 \item {\tt unlink_thy}, \bold{58} |
868 \item {\tt unlink_thy}, \bold{59} |
868 \item {\tt update}, \bold{58} |
869 \item {\tt update}, \bold{59} |
869 \item {\tt uresult}, \bold{9}, 11, 17 |
870 \item {\tt uresult}, \bold{9}, 11, 17 |
870 \item {\tt use}, \bold{3} |
871 \item {\tt use}, \bold{3} |
871 \item {\tt use_thy}, \bold{57} |
872 \item {\tt use_thy}, \bold{58} |
872 |
873 |
873 \indexspace |
874 \indexspace |
874 |
875 |
875 \item {\tt Var}, \bold{61}, 87 |
876 \item {\tt Var}, \bold{62}, 88 |
876 \item {\tt var} nonterminal, \bold{71, 72}, 85, 92 |
877 \item {\tt var} nonterminal, \bold{72, 73}, 86, 93 |
877 \item {\tt Variable}, 84 |
878 \item {\tt Variable}, 85 |
878 \item variables |
879 \item variables |
879 \subitem bound, \bold{61} |
880 \subitem bound, \bold{62} |
880 \subitem free, \bold{61} |
881 \subitem free, \bold{62} |
881 \item {\tt variant_abs}, \bold{62} |
882 \item {\tt variant_abs}, \bold{63} |
882 \item {\tt varifyT}, \bold{48} |
883 \item {\tt varifyT}, \bold{49} |
883 |
884 |
884 \indexspace |
885 \indexspace |
885 |
886 |
886 \item {\tt warning}, 5 |
887 \item {\tt warning}, 5 |
887 \item warnings, 5 |
888 \item warnings, 5 |
888 \item {\tt writeln}, 5 |
889 \item {\tt writeln}, 5 |
889 |
890 |
890 \indexspace |
891 \indexspace |
891 |
892 |
892 \item {\tt xnum} nonterminal, \bold{71}, 85, 92 |
893 \item {\tt xnum} nonterminal, \bold{72}, 86, 93 |
893 \item {\tt xstr} nonterminal, \bold{71}, 85, 92 |
894 \item {\tt xstr} nonterminal, \bold{72}, 86, 93 |
894 |
895 |
895 \indexspace |
896 \indexspace |
896 |
897 |
897 \item {\tt zero_var_indexes}, \bold{42} |
898 \item {\tt zero_var_indexes}, \bold{43} |
898 |
899 |
899 \end{theindex} |
900 \end{theindex} |