\begin{theindex}
\item {\tt !!} symbol, 69
\subitem in main goal, 8
\item {\tt\$}, \bold{60}, 86
\item {\tt\%} symbol, 69
\item {\tt ::} symbol, 69, 70
\item {\tt ==} symbol, 69
\item {\tt ==>} symbol, 69
\item {\tt =>} symbol, 69
\item {\tt =?=} symbol, 69
\item {\tt\at Enum} constant, 92
\item {\tt\at Finset} constant, 92, 93
\item {\tt [} symbol, 69
\item {\tt [|} symbol, 69
\item {\tt ]} symbol, 69
\item {\tt _K} constant, 94, 96
\item \verb'{}' symbol, 92
\item {\tt\ttlbrace} symbol, 69
\item {\tt\ttrbrace} symbol, 69
\item {\tt |]} symbol, 69
\indexspace
\item {\tt Abs}, \bold{60}, 86
\item {\tt abstract_over}, \bold{61}
\item {\tt abstract_rule}, \bold{45}
\item {\tt aconv}, \bold{61}
\item {\tt addaltern}, \bold{134}
\item {\tt addbefore}, \bold{133}
\item {\tt Addcongs}, \bold{105}
\item {\tt addcongs}, \bold{109}, 124, 125
\item {\tt AddDs}, \bold{138}
\item {\tt addDs}, \bold{132}
\item {\tt addeqcongs}, \bold{109}, 124
\item {\tt AddEs}, \bold{138}
\item {\tt addEs}, \bold{132}
\item {\tt AddIs}, \bold{138}
\item {\tt addIs}, \bold{132}
\item {\tt addloop}, \bold{112}
\item {\tt addSaltern}, \bold{133}
\item {\tt addSbefore}, \bold{133}
\item {\tt AddSDs}, \bold{138}
\item {\tt addSDs}, \bold{132}
\item {\tt AddSEs}, \bold{138}
\item {\tt addSEs}, \bold{132}
\item {\tt Addsimprocs}, \bold{105}
\item {\tt addsimprocs}, \bold{108}
\item {\tt Addsimps}, \bold{105}
\item {\tt addsimps}, \bold{108}, 125
\item {\tt AddSIs}, \bold{138}
\item {\tt addSIs}, \bold{132}
\item {\tt addSolver}, \bold{111}
\item {\tt addsplits}, \bold{112}, 124, 126
\item {\tt addss}, \bold{134}, 135
\item {\tt addSSolver}, \bold{111}
\item {\tt addSWrapper}, \bold{133}
\item {\tt addWrapper}, \bold{133}
\item {\tt all_tac}, \bold{31}
\item {\tt ALLGOALS}, \bold{35}, 116, 119
\item ambiguity
\subitem of parsed expressions, 79
\item {\tt ancestors_of}, \bold{59}
\item {\tt any} nonterminal, \bold{68}
\item {\tt APPEND}, \bold{29}, 31
\item {\tt APPEND'}, 36
\item {\tt Appl}, 83
\item {\tt aprop} nonterminal, \bold{70}
\item {\tt ares_tac}, \bold{20}
\item {\tt args} nonterminal, 93
\item {\tt Arith} theory, 118
\item arities
\subitem context conditions, 54
\item {\tt Asm_full_simp_tac}, \bold{104}
\item {\tt asm_full_simp_tac}, 23, \bold{112}, 117
\item {\tt asm_full_simplify}, 113
\item {\tt asm_rl} theorem, 22
\item {\tt Asm_simp_tac}, \bold{103}, 114
\item {\tt asm_simp_tac}, \bold{112}, 125
\item {\tt asm_simplify}, 113
\item associative-commutative operators, 118
\item {\tt assume}, \bold{44}
\item {\tt assume_ax}, 9, \bold{57}
\item {\tt assume_tac}, \bold{18}, 131
\item {\tt assumption}, \bold{47}
\item assumptions
\subitem contradictory, 138
\subitem deleting, 23
\subitem in simplification, 103, 111
\subitem inserting, 20
\subitem negated, 129
\subitem of main goal, 8--10, 15
\subitem reordering, 117
\subitem rotating, 23
\subitem substitution in, 100
\subitem tactics for, 18
\item ASTs, 83--88
\subitem made from parse trees, 84
\subitem made from terms, 86
\item {\tt atac}, \bold{20}
\item {\tt Auto_tac}, \bold{138}
\item {\tt auto_tac} $(cs,ss)$, \bold{136}
\item {\tt axclass} section, 53
\item axiomatic type class, 53
\item axioms
\subitem extracting, 57
\item {\tt axioms_of}, \bold{57}
\indexspace
\item {\tt ba}, \bold{12}
\item {\tt back}, \bold{10}
\item batch execution, 13
\item {\tt bd}, \bold{12}
\item {\tt bds}, \bold{12}
\item {\tt be}, \bold{12}
\item {\tt bes}, \bold{12}
\item {\tt BEST_FIRST}, \bold{32}, 33
\item {\tt Best_tac}, \bold{138}
\item {\tt best_tac}, \bold{136}
\item {\tt beta_conversion}, \bold{45}
\item {\tt bicompose}, \bold{48}
\item {\tt bimatch_tac}, \bold{24}
\item {\tt bind_thm}, \bold{9}, 10, 38
\item binders, \bold{78}
\item {\tt biresolution}, \bold{47}
\item {\tt biresolve_tac}, \bold{24}, 139
\item {\tt Blast.depth_tac}, \bold{135}
\item {\tt Blast.trace}, \bold{135}
\item {\tt Blast_tac}, \bold{138}
\item {\tt blast_tac}, \bold{135}
\item {\tt Bound}, \bold{60}, 84, 86, 87
\item {\tt bound_hyp_subst_tac}, \bold{100}
\item {\tt br}, \bold{12}
\item {\tt BREADTH_FIRST}, \bold{32}
\item {\tt brs}, \bold{12}
\item {\tt bw}, \bold{13}
\item {\tt bws}, \bold{13}
\item {\tt by}, \bold{8}, 10, 11, 16
\item {\tt byev}, \bold{8}
\indexspace
\item {\tt cd}, \bold{3}
\item {\tt cert_axm}, \bold{62}
\item {\tt CHANGED}, \bold{31}
\item {\tt chop}, \bold{10}, 14
\item {\tt choplev}, \bold{10}
\item {\tt Clarify_step_tac}, \bold{138}
\item {\tt clarify_step_tac}, \bold{134}
\item {\tt Clarify_tac}, \bold{138}
\item {\tt clarify_tac}, \bold{134}
\item claset
\subitem current, 138
\item {\tt claset} ML type, 131
\item classes
\subitem context conditions, 54
\item classical reasoner, 127--140
\subitem setting up, 139
\subitem tactics, 134
\item classical sets, 131
\item {\tt ClassicalFun}, 139
\item {\tt combination}, \bold{45}
\item {\tt commit}, \bold{2}
\item {\tt COMP}, \bold{47}
\item {\tt compose}, \bold{47}
\item {\tt compose_tac}, \bold{24}
\item {\tt concl_of}, \bold{41}
\item {\tt COND}, \bold{33}
\item congruence rules, 109
\item {\tt Const}, \bold{60}, 86, 96
\item {\tt Constant}, 83, 96
\item constants, \bold{60}
\subitem for translations, 73
\subitem syntactic, 88
\item {\tt context}, 103
\item {\tt contr_tac}, \bold{138}
\item {\tt could_unify}, \bold{26}
\item {\tt cprems_of}, \bold{41}
\item {\tt cprop_of}, \bold{40}
\item {\tt CPure} theory, 51
\item {\tt CPure.thy}, \bold{58}
\item {\tt crep_thm}, \bold{41}
\item {\tt cterm} ML type, 62
\item {\tt cterm_instantiate}, \bold{39}
\item {\tt cterm_of}, 8, 14, \bold{62}
\item {\tt ctyp}, \bold{63}
\item {\tt ctyp_of}, \bold{64}
\item {\tt cut_facts_tac}, 8, \bold{20}, 101
\item {\tt cut_inst_tac}, \bold{20}
\item {\tt cut_rl} theorem, 22
\indexspace
\item {\tt datatype}, 105
\item {\tt Deepen_tac}, \bold{138}
\item {\tt deepen_tac}, \bold{137}
\item {\tt defer_tac}, \bold{21}
\item definitions, \see{rewriting, meta-level}{1}, 21, \bold{54}
\subitem unfolding, 8, 9
\item {\tt Delcongs}, \bold{105}
\item {\tt delcongs}, \bold{109}
\item {\tt deleqcongs}, \bold{109}
\item {\tt delete_tmpfiles}, \bold{55}
\item delimiters, \bold{70}, 73, 74, 76
\item {\tt delrules}, \bold{132}
\item {\tt Delsimprocs}, \bold{105}
\item {\tt delsimprocs}, \bold{108}
\item {\tt Delsimps}, \bold{105}
\item {\tt delsimps}, \bold{108}
\item {\tt delSWrapper}, \bold{133}
\item {\tt delWrapper}, \bold{134}
\item {\tt dependent_tr'}, 94, \bold{96}
\item {\tt DEPTH_FIRST}, \bold{32}
\item {\tt DEPTH_SOLVE}, \bold{32}
\item {\tt DEPTH_SOLVE_1}, \bold{32}
\item {\tt depth_tac}, \bold{137}
\item {\tt Deriv.drop}, \bold{49}
\item {\tt Deriv.linear}, \bold{49}
\item {\tt Deriv.size}, \bold{49}
\item {\tt Deriv.tree}, \bold{49}
\item {\tt dest_eq}, \bold{101}
\item {\tt dest_imp}, \bold{101}
\item {\tt dest_state}, \bold{41}
\item {\tt dest_Trueprop}, \bold{101}
\item destruct-resolution, 18
\item {\tt DETERM}, \bold{33}
\item discrimination nets, \bold{25}
\item {\tt distinct_subgoals_tac}, \bold{23}
\item {\tt dmatch_tac}, \bold{18}
\item {\tt domain_type}, \bold{102}
\item {\tt dres_inst_tac}, \bold{19}
\item {\tt dresolve_tac}, \bold{18}
\item {\tt dtac}, \bold{20}
\item {\tt dummyT}, 86, 87, 97
\item duplicate subgoals
\subitem removing, 23
\indexspace
\item elim-resolution, 17
\item {\tt ematch_tac}, \bold{18}
\item {\tt empty} constant, 92
\item {\tt empty_cs}, \bold{132}
\item {\tt empty_ss}, \bold{107}
\item {\tt eq_assume_tac}, \bold{18}, 131
\item {\tt eq_assumption}, \bold{47}
\item {\tt eq_mp_tac}, \bold{139}
\item {\tt eq_reflection} theorem, \bold{102}, 122
\item {\tt eq_thm}, \bold{33}
\item {\tt eq_thy}, \bold{58}
\item {\tt equal_elim}, \bold{44}
\item {\tt equal_intr}, \bold{44}
\item equality, 99--102
\item {\tt eres_inst_tac}, \bold{19}
\item {\tt eresolve_tac}, \bold{17}
\subitem on other than first premise, 40
\item {\tt ERROR}, 5
\item {\tt error}, 5
\item error messages, 5
\item {\tt eta_contract}, \bold{5}, 90
\item {\tt etac}, \bold{20}
\item {\tt EVERY}, \bold{30}
\item {\tt EVERY'}, 36
\item {\tt EVERY1}, \bold{36}
\item examples
\subitem of logic definitions, 80
\subitem of macros, 92, 93
\subitem of mixfix declarations, 75
\subitem of simplification, 114
\subitem of translations, 96
\item exceptions
\subitem printing of, 5
\item {\tt exit}, \bold{2}
\item {\tt extensional}, \bold{45}
\indexspace
\item {\tt fa}, \bold{12}
\item {\tt Fast_tac}, \bold{138}
\item {\tt fast_tac}, \bold{136}
\item {\tt fd}, \bold{12}
\item {\tt fds}, \bold{12}
\item {\tt fe}, \bold{12}
\item {\tt fes}, \bold{12}
\item files
\subitem reading, 3, 55
\item {\tt filt_resolve_tac}, \bold{26}
\item {\tt FILTER}, \bold{31}
\item {\tt filter_goal}, \bold{16}
\item {\tt filter_thms}, \bold{26}
\item {\tt findE}, \bold{10}
\item {\tt findEs}, \bold{10}
\item {\tt findI}, \bold{10}
\item {\tt FIRST}, \bold{30}
\item {\tt FIRST'}, 36
\item {\tt FIRST1}, \bold{36}
\item {\tt FIRSTGOAL}, \bold{35}
\item flex-flex constraints, 23, 40, 48
\item {\tt flexflex_rule}, \bold{48}
\item {\tt flexflex_tac}, \bold{23}
\item {\tt FOL_basic_ss}, \bold{125}
\item {\tt FOL_ss}, \bold{125}
\item {\tt fold_goals_tac}, \bold{21}
\item {\tt fold_tac}, \bold{21}
\item {\tt forall_elim}, \bold{46}
\item {\tt forall_elim_list}, \bold{46}
\item {\tt forall_elim_var}, \bold{46}
\item {\tt forall_elim_vars}, \bold{46}
\item {\tt forall_intr}, \bold{45}
\item {\tt forall_intr_frees}, \bold{46}
\item {\tt forall_intr_list}, \bold{46}
\item {\tt force_strip_shyps}, \bold{41}
\item {\tt Force_tac}, \bold{138}
\item {\tt force_tac}, \bold{136}
\item {\tt forw_inst_tac}, \bold{19}
\item forward proof, 18, 38
\item {\tt forward_tac}, \bold{18}
\item {\tt fr}, \bold{12}
\item {\tt Free}, \bold{60}, 86
\item {\tt freezeT}, \bold{46}
\item {\tt frs}, \bold{12}
\item {\tt Full_simp_tac}, \bold{103}
\item {\tt full_simp_tac}, \bold{112}
\item {\tt full_simplify}, 113
\item {\textit {fun}} type, 63
\item function applications, \bold{60}
\indexspace
\item {\tt get_axiom}, \bold{57}
\item {\tt get_thm}, \bold{57}
\item {\tt get_thms}, \bold{57}
\item {\tt getgoal}, \bold{16}
\item {\tt gethyps}, \bold{16}, 34
\item {\tt goal}, \bold{8}, 14
\item {\tt goals_limit}, \bold{11}
\item {\tt goalw}, \bold{8}
\item {\tt goalw_cterm}, \bold{8}
\indexspace
\item {\tt has_fewer_prems}, \bold{33}
\item higher-order pattern, \bold{108}
\item {\tt HOL_basic_ss}, \bold{107}
\item {\tt hyp_subst_tac}, \bold{100}
\item {\tt hyp_subst_tacs}, \bold{140}
\item {\tt HypsubstFun}, 101, 140
\indexspace
\item {\tt id} nonterminal, \bold{70}, 84, 91
\item identifiers, 70
\item {\tt idt} nonterminal, 90
\item {\tt idts} nonterminal, \bold{70}, 78
\item {\tt IF_UNSOLVED}, \bold{33}
\item {\tt iff_reflection} theorem, 122
\item {\tt IFOL_ss}, \bold{125}
\item {\tt imp_intr} theorem, \bold{102}
\item {\tt implies_elim}, \bold{44}
\item {\tt implies_elim_list}, \bold{44}
\item {\tt implies_intr}, \bold{44}
\item {\tt implies_intr_hyps}, \bold{44}
\item {\tt implies_intr_list}, \bold{44}
\item {\tt incr_boundvars}, \bold{61}, 96
\item {\tt indexname} ML type, 60, 71
\item infixes, \bold{77}
\item {\tt insert} constant, 92
\item {\tt inst_step_tac}, \bold{137}
\item {\tt instance} section, 53
\item {\tt instantiate}, \bold{46}
\item {\tt instantiate'}, \bold{39}, 46
\item instantiation, 19, 39, 46
\item {\tt INTLEAVE}, \bold{29}, 31
\item {\tt INTLEAVE'}, 36
\item {\tt invoke_oracle}, \bold{64}
\item {\tt is} nonterminal, 92
\indexspace
\item {\tt joinrules}, \bold{139}
\indexspace
\item {\tt keep_derivs}, \bold{49}
\indexspace
\item $\lambda$-abstractions, 25, \bold{60}
\item $\lambda$-calculus, 43, 45, 70
\item {\tt lessb}, \bold{25}
\item lexer, \bold{70}
\item {\tt lift_rule}, \bold{48}
\item lifting, 48
\item {\tt loadpath}, \bold{55}
\item {\tt logic} class, 70, 75
\item {\tt logic} nonterminal, \bold{70}
\item {\tt Logic.auto_rename}, \bold{23}
\item {\tt Logic.set_rename_prefix}, \bold{22}
\item {\tt long_names}, \bold{4}
\item {\tt loose_bnos}, \bold{61}, 97
\indexspace
\item macros, 88--94
\item {\tt make_elim}, \bold{40}, 132
\item {\tt Match} exception, 95
\item {\tt match_tac}, \bold{18}, 131
\item {\tt max_pri}, 68, \bold{74}
\item {\tt merge_ss}, \bold{107}
\item {\tt merge_theories}, \bold{58}
\item meta-assumptions, 34, 42, 44, 47
\subitem printing of, 4
\item meta-equality, 43--45
\item meta-implication, 43, 44
\item meta-quantifiers, 43, 45
\item meta-rewriting, 8, 13, 14, \bold{21},
\seealso{tactics, theorems}{141}
\subitem in theorems, 39
\item meta-rules, \see{meta-rules}{1}, 42--48
\item {\tt METAHYPS}, 16, \bold{34}
\item mixfix declarations, 52, 73--78
\item {\tt mk_case_split_tac}, \bold{125}
\item {\tt mk_simproc}, \bold{120}
\item {\tt ML} section, 53, 95, 97
\item model checkers, 79
\item {\tt mp} theorem, \bold{139}
\item {\tt mp_tac}, \bold{139}
\item {\tt MRL}, \bold{38}
\item {\tt MRS}, \bold{38}
\indexspace
\item name tokens, \bold{70}
\item {\tt nat_cancel}, \bold{109}
\item {\tt net_bimatch_tac}, \bold{25}
\item {\tt net_biresolve_tac}, \bold{25}
\item {\tt net_match_tac}, \bold{25}
\item {\tt net_resolve_tac}, \bold{25}
\item {\tt no_tac}, \bold{31}
\item {\tt None}, \bold{27}
\item {\tt not_elim} theorem, \bold{140}
\item {\tt nprems_of}, \bold{41}
\item numerals, 70
\indexspace
\item {\textit {o}} type, 80
\item {\tt object}, 64
\item {\tt op} symbol, 77
\item {\tt option} ML type, 27
\item oracles, 64--66
\item {\tt ORELSE}, \bold{29}, 31, 35
\item {\tt ORELSE'}, 36
\indexspace
\item parameters
\subitem removing unused, 23
\subitem renaming, 13, 22, 48
\item {\tt parents_of}, \bold{59}
\item parse trees, 83
\item {\tt parse_rules}, 90
\item pattern, higher-order, \bold{108}
\item {\tt pause_tac}, \bold{27}
\item Poly/{\ML} compiler, 5
\item {\tt pop_proof}, \bold{15}
\item {\tt pr}, \bold{11}
\item {\tt premises}, \bold{8}, 15
\item {\tt prems_of}, \bold{41}
\item {\tt prems_of_ss}, \bold{110}
\item pretty printing, 74, 76--77, 93
\item {\tt Pretty.setdepth}, \bold{4}
\item {\tt Pretty.setmargin}, \bold{4}
\item {\tt PRIMITIVE}, \bold{26}
\item {\tt primrec}, 105
\item {\tt prin}, 6, \bold{15}
\item print mode, 52, 97
\item print modes, 78--79
\item {\tt print_cs}, \bold{132}
\item {\tt print_data}, \bold{59}
\item {\tt print_depth}, \bold{4}
\item {\tt print_exn}, \bold{6}, 37
\item {\tt print_goals}, \bold{38}
\item {\tt print_mode}, 78
\item {\tt print_modes}, 73
\item {\tt print_rules}, 90
\item {\tt print_simpset}, \bold{107}
\item {\tt print_ss}, \bold{106}
\item {\tt print_syntax}, \bold{59}, \bold{72}
\item {\tt print_tac}, \bold{27}
\item {\tt print_theory}, \bold{59}
\item {\tt print_thm}, \bold{38}
\item printing control, 3--5
\item {\tt printyp}, \bold{15}
\item priorities, 67, \bold{74}
\item priority grammars, 67--68
\item {\tt prlev}, \bold{11}
\item {\tt prlim}, \bold{11}
\item productions, 67, 73, 74
\subitem copy, \bold{73}, 74, 85
\item {\tt proof} ML type, 15
\item proof objects, 48--50
\item proof state, 7
\subitem printing of, 11
\item {\tt proof_timing}, \bold{11}
\item proofs, 7--16
\subitem inspecting the state, 16
\subitem managing multiple, 14
\subitem saving and restoring, 15
\subitem stacking, 14
\subitem starting, 7
\subitem timing, 11
\item {\tt PROP} symbol, 69
\item {\textit {prop}} type, 63, 70
\item {\tt prop} nonterminal, \bold{68}, 80
\item {\tt ProtoPure.thy}, \bold{58}
\item {\tt prove_goal}, 11, \bold{14}
\item {\tt prove_goalw}, \bold{14}
\item {\tt prove_goalw_cterm}, \bold{14}
\item {\tt prth}, \bold{37}
\item {\tt prthq}, \bold{38}
\item {\tt prths}, \bold{38}
\item {\tt prune_params_tac}, \bold{23}
\item {\tt pttrn} nonterminal, \bold{70}
\item {\tt pttrns} nonterminal, \bold{70}
\item {\tt Pure} theory, 51, 68, 72
\item {\tt Pure.thy}, \bold{58}
\item {\tt push_proof}, \bold{15}
\item {\tt pwd}, \bold{3}
\indexspace
\item {\tt qed}, \bold{9}, 10, 57
\item {\tt qed_goal}, \bold{14}
\item {\tt qed_goalw}, \bold{14}
\item quantifiers, 78
\item {\tt quit}, \bold{2}
\indexspace
\item {\tt read}, \bold{15}
\item {\tt read_axm}, \bold{62}
\item {\tt read_cterm}, \bold{62}
\item {\tt read_instantiate}, \bold{39}
\item {\tt read_instantiate_sg}, \bold{39}
\item reading
\subitem axioms, \see{{\tt assume_ax}}{51}
\subitem goals, \see{proofs, starting}{7}
\item {\tt reflexive}, \bold{45}
\item {\tt ren}, \bold{13}
\item {\tt rename_last_tac}, \bold{22}
\item {\tt rename_params_rule}, \bold{48}
\item {\tt rename_tac}, \bold{22}
\item {\tt rep_cs}, \bold{132}
\item {\tt rep_cterm}, \bold{62}
\item {\tt rep_ctyp}, \bold{64}
\item {\tt rep_ss}, \bold{106}
\item {\tt rep_thm}, \bold{41}
\item {\tt REPEAT}, \bold{30, 31}
\item {\tt REPEAT1}, \bold{30}
\item {\tt REPEAT_DETERM}, \bold{30}
\item {\tt REPEAT_FIRST}, \bold{35}
\item {\tt REPEAT_SOME}, \bold{35}
\item {\tt res_inst_tac}, \bold{19}, 23, 24
\item reserved words, 70, 93
\item {\tt reset}, 3
\item resolution, 38, 47
\subitem tactics, 17
\subitem without lifting, 47
\item {\tt resolve_tac}, \bold{17}, 131
\item {\tt restore_proof}, \bold{15}
\item {\tt result}, \bold{9}, 16, 57
\item {\tt rev_mp} theorem, \bold{102}
\item rewrite rules, 107--108
\subitem permutative, 117--120
\item {\tt rewrite_goals_rule}, \bold{39}
\item {\tt rewrite_goals_tac}, \bold{21}, 39
\item {\tt rewrite_rule}, \bold{39}
\item {\tt rewrite_tac}, 9, \bold{21}
\item rewriting
\subitem object-level, \see{simplification}{1}
\subitem ordered, 117
\subitem syntactic, 88--94
\item {\tt rewtac}, \bold{20}
\item {\tt RL}, \bold{38}
\item {\tt RLN}, \bold{38}
\item {\tt rotate_prems}, \bold{40}
\item {\tt rotate_proof}, \bold{15}
\item {\tt rotate_tac}, \bold{23}
\item {\tt RS}, \bold{38}
\item {\tt RSN}, \bold{38}
\item {\tt rtac}, \bold{20}
\item {\tt rule_by_tactic}, 23, \bold{40}
\item rules
\subitem converting destruction to elimination, 40
\indexspace
\item {\tt safe_asm_full_simp_tac}, \bold{113}
\item {\tt Safe_step_tac}, \bold{138}
\item {\tt safe_step_tac}, 133, \bold{137}
\item {\tt Safe_tac}, \bold{138}
\item {\tt safe_tac}, \bold{137}
\item {\tt save_proof}, \bold{15}
\item saving your work, \bold{1}
\item search, 29
\subitem tacticals, 31--33
\item {\tt SELECT_GOAL}, 21, \bold{34}
\item {\tt Seq.seq} ML type, 26
\item sequences (lazy lists), \bold{27}
\item sequent calculus, 128
\item sessions, 1--6
\item {\tt set}, 3
\item {\tt setloop}, \bold{112}
\item {\tt setmksimps}, 108, \bold{123}, 125
\item {\tt setSolver}, \bold{111}, 125
\item {\tt setSSolver}, \bold{111}, 125
\item {\tt setsubgoaler}, \bold{110}, 125
\item {\tt settermless}, \bold{117}
\item shortcuts
\subitem for tactics, 20
\subitem for {\tt by} commands, 11
\item {\tt show_brackets}, \bold{4}
\item {\tt show_consts}, \bold{4}
\item {\tt show_hyps}, \bold{4}
\item {\tt show_sorts}, \bold{4}, 87, 95
\item {\tt show_types}, \bold{4}, 87, 90, 97
\item {\tt Sign.certify_term}, \bold{62}
\item {\tt Sign.certify_typ}, \bold{64}
\item {\tt Sign.sg} ML type, 51
\item {\tt Sign.stamp_names_of}, \bold{59}
\item {\tt Sign.string_of_term}, \bold{62}
\item {\tt Sign.string_of_typ}, \bold{63}
\item {\tt sign_of}, 8, 14, \bold{59}
\item {\tt sign_of_thm}, \bold{41}
\item signatures, \bold{51}, 59, 61, 62, 64
\item {\tt Simp_tac}, \bold{103}
\item {\tt simp_tac}, \bold{112}
\item simplification, 103--126
\subitem forward rules, 113
\subitem from classical reasoner, 134
\subitem setting up, 121
\subitem tactics, 112
\item simplification sets, 106
\item {\tt simplify}, 113
\item {\tt SIMPSET}, \bold{113}
\item simpset
\subitem current, 103, 107
\item {\tt simpset}, \bold{107}
\item {\tt SIMPSET'}, \bold{113}
\item {\tt simpset_of}, \bold{107}
\item {\tt simpset_ref}, \bold{107}
\item {\tt simpset_ref_of}, \bold{107}
\item {\tt simpset_thy_data}, \bold{126}
\item {\tt size_of_thm}, 32, \bold{33}, 140
\item {\tt sizef}, \bold{140}
\item {\tt slow_best_tac}, \bold{136}
\item {\tt slow_step_tac}, 133, \bold{137}
\item {\tt slow_tac}, \bold{136}
\item {\tt Some}, \bold{27}
\item {\tt SOMEGOAL}, \bold{35}
\item {\tt sort} nonterminal, \bold{70}
\item sort constraints, 69
\item sort hypotheses, 41
\item sorts
\subitem printing of, 4
\item {\tt split_tac}, \bold{125}
\item {\tt ssubst} theorem, \bold{99}
\item {\tt stac}, \bold{100}
\item stamps, \bold{51}, 59
\item {\tt standard}, \bold{40}
\item starting up, \bold{1}
\item {\tt Step_tac}, \bold{138}
\item {\tt step_tac}, 133, \bold{137}
\item {\tt store_thm}, \bold{9}
\item {\tt string_of_cterm}, \bold{62}
\item {\tt string_of_ctyp}, \bold{63}
\item {\tt string_of_thm}, \bold{38}
\item strings, 70
\item {\tt SUBGOAL}, \bold{26}
\item subgoal module, 7--16
\item {\tt subgoal_tac}, \bold{20}
\item {\tt subgoals_of_brl}, \bold{24}
\item {\tt subgoals_tac}, \bold{21}
\item {\tt subst} theorem, 99, \bold{102}
\item substitution
\subitem rules, 99
\item {\tt subthy}, \bold{58}
\item {\tt swap} theorem, \bold{140}
\item {\tt swap_res_tac}, \bold{139}
\item {\tt swapify}, \bold{139}
\item {\tt sym} theorem, 100, \bold{102}
\item {\tt symmetric}, \bold{45}
\item {\tt syn_of}, \bold{72}
\item syntax
\subitem Pure, 68--73
\subitem transformations, 83--97
\item {\tt syntax} section, 52
\item {\tt Syntax.ast} ML type, 83
\item {\tt Syntax.mark_boundT}, 97
\item {\tt Syntax.print_gram}, \bold{72}
\item {\tt Syntax.print_syntax}, \bold{72}
\item {\tt Syntax.print_trans}, \bold{72}
\item {\tt Syntax.stat_norm_ast}, 92
\item {\tt Syntax.syntax} ML type, 72
\item {\tt Syntax.test_read}, 76, 92
\item {\tt Syntax.trace_norm_ast}, 92
\item {\tt Syntax.variant_abs'}, 97
\indexspace
\item {\tt tactic} ML type, 17
\item tacticals, 29--36
\subitem conditional, 33
\subitem deterministic, 33
\subitem for filtering, 31
\subitem for restriction to a subgoal, 34
\subitem identities for, 30
\subitem joining a list of tactics, 30
\subitem joining tactic functions, 36
\subitem joining two tactics, 29
\subitem repetition, 30
\subitem scanning for subgoals, 35
\subitem searching, 32
\item tactics, 17--28
\subitem assumption, \bold{18}, 20
\subitem commands for applying, 8
\subitem debugging, 15
\subitem filtering results of, 31
\subitem for composition, 24
\subitem for contradiction, 138
\subitem for inserting facts, 20
\subitem for Modus Ponens, 138
\subitem instantiation, 19
\subitem matching, 18
\subitem meta-rewriting, 20, \bold{21}
\subitem primitives for coding, 26
\subitem resolution, \bold{17}, 20, 24, 25
\subitem restricting to a subgoal, 34
\subitem simplification, 112
\subitem substitution, 99--102
\subitem tracing, 27
\item {\tt TERM}, 62
\item {\tt term} ML type, 60, 86
\item terms, \bold{60}
\subitem certified, \bold{61}
\subitem made from ASTs, 86
\subitem printing of, 15, 62
\subitem reading of, 15
\item {\tt TFree}, \bold{63}
\item {\tt THEN}, \bold{29}, 31, 35
\item {\tt THEN'}, 36
\item {\tt THEN_BEST_FIRST}, \bold{32}
\item theorems, 37--50
\subitem equality of, 33
\subitem extracting, 57
\subitem extracting proved, 9
\subitem joining by resolution, 38
\subitem of pure theory, 22
\subitem printing of, 37
\subitem retrieving, 10
\subitem size of, 33
\subitem standardizing, 40
\subitem storing, 9
\subitem taking apart, 40
\item theories, 51--66
\subitem axioms of, 57
\subitem constructing, \bold{58}
\subitem inspecting, \bold{59}
\subitem loading, 55
\subitem parent, \bold{51}
\subitem pseudo, \bold{56}
\subitem reloading, \bold{55}
\subitem removing, \bold{56}
\subitem theorems of, 57
\item {\tt THEORY} exception, 51, 57
\item {\tt theory} ML type, 51
\item {\tt Theory.add_oracle}, \bold{64}
\item {\tt theory_of_thm}, \bold{41}
\item {\tt thin_refl} theorem, \bold{102}
\item {\tt thin_tac}, \bold{23}
\item {\tt THM} exception, 37, 38, 42, 47
\item {\tt thm} ML type, 37
\item {\tt thms_containing}, \bold{10}
\item {\tt thms_of}, \bold{57}
\item {\tt thy_data}, \bold{126}
\item {\tt tid} nonterminal, \bold{70}, 84, 91
\item {\tt time_use}, \bold{3}
\item {\tt time_use_thy}, \bold{55}
\item timing statistics, 11
\item {\tt toggle}, 3
\item token class, 97
\item token translations, 97--98
\item token_translation, 98
\item {\tt token_translation}, 98
\item {\tt topthm}, \bold{16}
\item {\tt tpairs_of}, \bold{41}
\item {\tt trace_BEST_FIRST}, \bold{32}
\item {\tt trace_DEPTH_FIRST}, \bold{32}
\item {\tt trace_goalno_tac}, \bold{35}
\item {\tt trace_REPEAT}, \bold{30}
\item {\tt trace_simp}, \bold{104}, 115
\item tracing
\subitem of classical prover, 135
\subitem of macros, 92
\subitem of searching tacticals, 32
\subitem of simplification, 105, 115--116
\subitem of tactics, 27
\subitem of unification, 42
\item {\tt transfer}, \bold{58}
\item {\tt transfer_sg}, \bold{58}
\item {\tt transitive}, \bold{45}
\item translations, 94--97
\subitem parse, 78, 86
\subitem parse AST, \bold{84}, 85
\subitem print, 78
\subitem print AST, \bold{87}
\item {\tt translations} section, 89
\item {\tt trivial}, \bold{48}
\item {\tt Trueprop} constant, 80
\item {\tt TRY}, \bold{30, 31}
\item {\tt TRYALL}, \bold{35}
\item {\tt TVar}, \bold{63}
\item {\tt tvar} nonterminal, \bold{70, 71}, 84, 91
\item {\tt typ} ML type, 63
\item {\tt Type}, \bold{63}
\item {\textit {type}} type, 75
\item {\tt type} nonterminal, \bold{70}
\item type constraints, 70, 78, 87
\item type constructors, \bold{63}
\item type identifiers, 70
\item type synonyms, \bold{52}
\item type unknowns, \bold{63}, 70
\subitem freezing/thawing of, 46
\item type variables, \bold{63}
\item types, \bold{63}
\subitem certified, \bold{63}
\subitem printing of, 4, 15, 63
\indexspace
\item {\tt undo}, 7, \bold{10}, 14
\item unknowns, \bold{60}, 70
\item {\tt unlink_thy}, \bold{56}
\item {\tt update}, \bold{56}
\item {\tt uresult}, \bold{9}, 16, 57
\item {\tt use}, \bold{3}
\item {\tt use_thy}, \bold{55}
\indexspace
\item {\tt Var}, \bold{60}, 86
\item {\tt var} nonterminal, \bold{70, 71}, 84, 91
\item {\tt Variable}, 83
\item variables
\subitem bound, \bold{60}
\subitem free, \bold{60}
\item {\tt variant_abs}, \bold{61}
\item {\tt varifyT}, \bold{46}
\indexspace
\item {\tt warning}, 5
\item warnings, 5
\item {\tt writeln}, 5
\indexspace
\item {\tt xnum} nonterminal, \bold{70}, 84, 91
\item {\tt xstr} nonterminal, \bold{70}, 84, 91
\indexspace
\item {\tt zero_var_indexes}, \bold{40}
\end{theindex}