added index info;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/logics.ind	Thu Feb 20 16:09:41 1997 +0100
@@ -0,0 +1,974 @@
+\begin{theindex}
+
+  \item {\ptt !} symbol, 59, 61, 67, 69
+  \item {\tt[]} symbol, 80
+  \item {\tt\#} symbol, 80
+  \item {\tt\#*} symbol, 46, 122
+  \item {\tt\#+} symbol, 46, 122
+  \item {\tt\#-} symbol, 46
+  \item {\tt\&} symbol, 6, 59, 99
+  \item {\ptt *} symbol, 25, 60, 78, 113
+  \item {\ptt *} type, 75
+  \item {\ptt +} symbol, 42, 60, 78, 113
+  \item {\ptt +} type, 75
+  \item {\ptt -} symbol, 24, 60, 78, 122
+  \item {\ptt -->} symbol, 6, 59, 99, 113
+  \item {\ptt ->} symbol, 25
+  \item {\ptt -``} symbol, 24
+  \item {\ptt :} symbol, 24, 66
+  \item {\ptt <} symbol, 78
+  \item {\ptt <->} symbol, 6, 99
+  \item {\ptt <=} symbol, 24, 66
+  \item {\ptt =} symbol, 6, 59, 99, 113
+  \item {\ptt ?} symbol, 59, 61, 67, 69
+  \item {\ptt ?!} symbol, 59
+  \item {\tt\at} symbol, 59, 80
+  \item {\ptt `} symbol, 24, 113
+  \item {\ptt ``} symbol, 24, 66
+  \item \verb'{}' symbol, 66
+  \item {\ptt |} symbol, 6, 59, 99
+  \item {\ptt |-|} symbol, 122
+
+  \indexspace
+
+  \item {\ptt 0} constant, 24, 78, 111
+
+  \indexspace
+
+  \item {\ptt absdiff_def} theorem, 122
+  \item {\ptt add_0} theorem, 79
+  \item {\ptt add_assoc} theorem, 122
+  \item {\ptt add_commute} theorem, 122
+  \item {\ptt add_def} theorem, 46, 122
+  \item {\ptt add_inverse_diff} theorem, 122
+  \item {\ptt add_mp_tac}, \bold{121}
+  \item {\ptt add_mult_dist} theorem, 46, 122
+  \item {\ptt add_safes}, \bold{105}
+  \item {\ptt add_Suc} theorem, 79
+  \item {\ptt add_typing} theorem, 122
+  \item {\ptt add_unsafes}, \bold{105}
+  \item {\ptt addC0} theorem, 122
+  \item {\ptt addC_succ} theorem, 122
+  \item {\ptt ALL} symbol, 6, 25, 59, 61, 67, 69, 99
+  \item {\ptt All} constant, 6, 59, 99
+  \item {\ptt All_def} theorem, 62
+  \item {\ptt all_dupE} theorem, 4, 8, 65
+  \item {\ptt all_impE} theorem, 8
+  \item {\ptt allE} theorem, 4, 8, 65
+  \item {\ptt allI} theorem, 7, 65
+  \item {\ptt allL} theorem, 101, 104
+  \item {\ptt allL_thin} theorem, 102
+  \item {\ptt allR} theorem, 101
+  \item {\ptt and_def} theorem, 42, 62
+  \item {\ptt app_def} theorem, 48
+  \item {\ptt append_Cons} theorem, 81
+  \item {\ptt append_Nil} theorem, 81
+  \item {\ptt apply_def} theorem, 30
+  \item {\ptt apply_equality} theorem, 38, 40, 56
+  \item {\ptt apply_equality2} theorem, 38
+  \item {\ptt apply_iff} theorem, 38
+  \item {\ptt apply_Pair} theorem, 38, 56
+  \item {\ptt apply_type} theorem, 38
+  \item {\ptt arg_cong} theorem, 64
+  \item {\ptt Arith} theory, 43, 77, 121
+  \item assumptions
+    \subitem contradictory, 15
+    \subitem in {\CTT}, 110, 120
+
+  \indexspace
+
+  \item {\ptt Ball} constant, 24, 28, 66, 69
+  \item {\ptt ball_cong} theorem, 31, 32
+  \item {\ptt Ball_def} theorem, 29, 69
+  \item {\ptt ballE} theorem, 31, 32, 70
+  \item {\ptt ballI} theorem, 32, 70
+  \item {\ptt basic} theorem, 101
+  \item {\ptt basic_defs}, \bold{119}
+  \item {\ptt best_tac}, \bold{106}
+  \item {\ptt beta} theorem, 39, 40
+  \item {\ptt Bex} constant, 24, 28, 66, 69
+  \item {\ptt bex_cong} theorem, 31, 32
+  \item {\ptt Bex_def} theorem, 29, 69
+  \item {\ptt bexCI} theorem, 32, 70, 72
+  \item {\ptt bexE} theorem, 32, 70
+  \item {\ptt bexI} theorem, 32, 70, 72
+  \item {\ptt bij} constant, 45
+  \item {\ptt bij_converse_bij} theorem, 45
+  \item {\ptt bij_def} theorem, 45
+  \item {\ptt bij_disjoint_Un} theorem, 45
+  \item {\ptt bnd_mono_def} theorem, 44
+  \item {\ptt Bool} theory, 40
+  \item {\ptt bool} type, 60
+  \item {\ptt bool_0I} theorem, 42
+  \item {\ptt bool_1I} theorem, 42
+  \item {\ptt bool_def} theorem, 42
+  \item {\ptt boolE} theorem, 42
+  \item {\ptt box_equals} theorem, 63, 64
+  \item {\ptt bspec} theorem, 32, 70
+
+  \indexspace
+
+  \item {\ptt case} constant, 42
+  \item {\ptt case} symbol, 61, 82, 86
+  \item {\ptt case_def} theorem, 42
+  \item {\ptt case_Inl} theorem, 42
+  \item {\ptt case_Inr} theorem, 42
+  \item {\ptt case_tac}, \bold{63}
+  \item {\ptt CCL} theory, 1
+  \item {\ptt ccontr} theorem, 65
+  \item {\ptt classical} theorem, 65
+  \item {\ptt coinduct} theorem, 44
+  \item {\ptt coinductive}, 91--94
+  \item {\ptt Collect} constant, 24, 25, 28, 66, 68
+  \item {\ptt Collect_def} theorem, 29
+  \item {\ptt Collect_mem_eq} theorem, 69
+  \item {\ptt Collect_subset} theorem, 35
+  \item {\ptt CollectD} theorem, 70, 96
+  \item {\ptt CollectD1} theorem, 31, 33
+  \item {\ptt CollectD2} theorem, 31, 33
+  \item {\ptt CollectE} theorem, 31, 33, 70
+  \item {\ptt CollectI} theorem, 33, 70, 97
+  \item {\ptt comp_assoc} theorem, 45
+  \item {\ptt comp_bij} theorem, 45
+  \item {\ptt comp_def} theorem, 45
+  \item {\ptt comp_func} theorem, 45
+  \item {\ptt comp_func_apply} theorem, 45
+  \item {\ptt comp_inj} theorem, 45
+  \item {\ptt comp_rls}, \bold{119}
+  \item {\ptt comp_surj} theorem, 45
+  \item {\ptt comp_type} theorem, 45
+  \item {\ptt Compl} constant, 66
+  \item {\ptt Compl_def} theorem, 69
+  \item {\ptt Compl_disjoint} theorem, 73
+  \item {\ptt Compl_Int} theorem, 73
+  \item {\ptt Compl_partition} theorem, 73
+  \item {\ptt Compl_Un} theorem, 73
+  \item {\ptt ComplD} theorem, 71
+  \item {\ptt ComplI} theorem, 71
+  \item {\ptt cond_0} theorem, 42
+  \item {\ptt cond_1} theorem, 42
+  \item {\ptt cond_def} theorem, 42
+  \item {\ptt cong} theorem, 64
+  \item congruence rules, 31
+  \item {\ptt conj_cong}, 74
+  \item {\ptt conj_impE} theorem, 5, 8
+  \item {\ptt conjE} theorem, 8, 64
+  \item {\ptt conjI} theorem, 7, 64
+  \item {\ptt conjL} theorem, 101
+  \item {\ptt conjR} theorem, 101
+  \item {\ptt conjunct1} theorem, 7, 64
+  \item {\ptt conjunct2} theorem, 7, 64
+  \item {\ptt conL} theorem, 102
+  \item {\ptt conR} theorem, 102
+  \item {\ptt cons} constant, 24, 25
+  \item {\ptt cons_def} theorem, 30
+  \item {\ptt Cons_iff} theorem, 48
+  \item {\ptt consCI} theorem, 34
+  \item {\ptt consE} theorem, 34
+  \item {\ptt ConsI} theorem, 48
+  \item {\ptt consI1} theorem, 34
+  \item {\ptt consI2} theorem, 34
+  \item Constructive Type Theory, 110--133
+  \item {\ptt contr} constant, 111
+  \item {\ptt converse} constant, 24, 37
+  \item {\ptt converse_def} theorem, 30
+  \item {\ptt could_res}, \bold{103}
+  \item {\ptt could_resolve_seq}, \bold{104}
+  \item {\ptt CTT} theory, 1, 110
+  \item {\ptt Cube} theory, 1
+  \item {\ptt cut} theorem, 101
+  \item {\ptt cut_facts_tac}, 17, 18, 55
+  \item {\ptt cutL_tac}, \bold{103}
+  \item {\ptt cutR_tac}, \bold{103}
+
+  \indexspace
+
+  \item {\ptt datatype}, 85--91
+  \item {\ptt deepen_tac}, 15
+  \item {\ptt diff_0} theorem, 79
+  \item {\ptt diff_0_eq_0} theorem, 79, 122
+  \item {\ptt Diff_cancel} theorem, 41
+  \item {\ptt Diff_contains} theorem, 35
+  \item {\ptt Diff_def} theorem, 29
+  \item {\ptt diff_def} theorem, 46, 122
+  \item {\ptt Diff_disjoint} theorem, 41
+  \item {\ptt Diff_Int} theorem, 41
+  \item {\ptt Diff_partition} theorem, 41
+  \item {\ptt diff_self_eq_0} theorem, 122
+  \item {\ptt Diff_subset} theorem, 35
+  \item {\ptt diff_Suc_Suc} theorem, 79
+  \item {\ptt diff_succ_succ} theorem, 122
+  \item {\ptt diff_typing} theorem, 122
+  \item {\ptt Diff_Un} theorem, 41
+  \item {\ptt diffC0} theorem, 122
+  \item {\ptt DiffD1} theorem, 34
+  \item {\ptt DiffD2} theorem, 34
+  \item {\ptt DiffE} theorem, 34
+  \item {\ptt DiffI} theorem, 34
+  \item {\ptt disj_impE} theorem, 5, 8, 13
+  \item {\ptt disjCI} theorem, 10, 65
+  \item {\ptt disjE} theorem, 7, 64
+  \item {\ptt disjI1} theorem, 7, 64
+  \item {\ptt disjI2} theorem, 7, 64
+  \item {\ptt disjL} theorem, 101
+  \item {\ptt disjR} theorem, 101
+  \item {\ptt div} symbol, 46, 78, 122
+  \item {\ptt div_def} theorem, 46, 122
+  \item {\ptt div_geq} theorem, 79
+  \item {\ptt div_less} theorem, 79
+  \item {\ptt domain} constant, 24, 38
+  \item {\ptt domain_def} theorem, 30
+  \item {\ptt domain_of_fun} theorem, 38
+  \item {\ptt domain_subset} theorem, 37
+  \item {\ptt domain_type} theorem, 38
+  \item {\ptt domainE} theorem, 37, 38
+  \item {\ptt domainI} theorem, 37, 38
+  \item {\ptt double_complement} theorem, 41, 73
+  \item {\ptt dresolve_tac}, 53
+
+  \indexspace
+
+  \item {\ptt Elem} constant, 111
+  \item {\ptt elim_rls}, \bold{119}
+  \item {\ptt elimL_rls}, \bold{119}
+  \item {\ptt empty_def} theorem, 69
+  \item {\ptt empty_pack}, \bold{104}
+  \item {\ptt empty_subsetI} theorem, 32
+  \item {\ptt emptyE} theorem, 32, 71
+  \item {\ptt Eps} constant, 59, 61
+  \item {\ptt Eq} constant, 111
+  \item {\ptt eq} constant, 111, 118
+  \item {\ptt eq_mp_tac}, \bold{9}
+  \item {\ptt EqC} theorem, 118
+  \item {\ptt EqE} theorem, 118
+  \item {\ptt Eqelem} constant, 111
+  \item {\ptt EqF} theorem, 118
+  \item {\ptt EqFL} theorem, 118
+  \item {\ptt EqI} theorem, 118
+  \item {\ptt Eqtype} constant, 111
+  \item {\ptt equal_tac}, \bold{120}
+  \item {\ptt equal_types} theorem, 114
+  \item {\ptt equal_typesL} theorem, 114
+  \item {\ptt equalityCE} theorem, 70, 72, 96, 97
+  \item {\ptt equalityD1} theorem, 32, 70
+  \item {\ptt equalityD2} theorem, 32, 70
+  \item {\ptt equalityE} theorem, 32, 70
+  \item {\ptt equalityI} theorem, 32, 52, 54, 70
+  \item {\ptt equals0D} theorem, 32
+  \item {\ptt equals0I} theorem, 32
+  \item {\ptt eresolve_tac}, 15
+  \item {\ptt eta} theorem, 39, 40
+  \item {\ptt EX} symbol, 6, 25, 59, 61, 67, 69, 99
+  \item {\ptt Ex} constant, 6, 59, 99
+  \item {\ptt EX!} symbol, 6, 59
+  \item {\ptt Ex1} constant, 6, 59
+  \item {\ptt Ex1_def} theorem, 62
+  \item {\ptt ex1_def} theorem, 7
+  \item {\ptt ex1E} theorem, 8, 65
+  \item {\ptt ex1I} theorem, 8, 65
+  \item {\ptt Ex_def} theorem, 62
+  \item {\ptt ex_impE} theorem, 8
+  \item {\ptt exCI} theorem, 10, 14, 65
+  \item {\ptt excluded_middle} theorem, 10, 65
+  \item {\ptt exE} theorem, 7, 65
+  \item {\ptt exI} theorem, 7, 65
+  \item {\ptt exL} theorem, 101
+  \item {\ptt expand_if} theorem, 65
+  \item {\ptt expand_split} theorem, 75
+  \item {\ptt expand_sum_case} theorem, 77
+  \item {\ptt exR} theorem, 101, 104, 106
+  \item {\ptt exR_thin} theorem, 102, 106, 107
+  \item {\ptt ext} theorem, 62, 63
+  \item {\ptt extension} theorem, 29
+
+  \indexspace
+
+  \item {\ptt F} constant, 111
+  \item {\ptt f_Inv_f} theorem, 72
+  \item {\ptt False} constant, 6, 59, 99
+  \item {\ptt False_def} theorem, 62
+  \item {\ptt FalseE} theorem, 7, 64
+  \item {\ptt FalseL} theorem, 101
+  \item {\ptt Fast_tac}, 53
+  \item {\ptt fast_tac}, 17, 19, 20, 55, \bold{106}
+  \item {\ptt FE} theorem, 117, 121
+  \item {\ptt FEL} theorem, 117
+  \item {\ptt FF} theorem, 117
+  \item {\ptt field} constant, 24
+  \item {\ptt field_def} theorem, 30
+  \item {\ptt field_subset} theorem, 37
+  \item {\ptt fieldCI} theorem, 37
+  \item {\ptt fieldE} theorem, 37
+  \item {\ptt fieldI1} theorem, 37
+  \item {\ptt fieldI2} theorem, 37
+  \item {\ptt filseq_resolve_tac}, \bold{104}
+  \item {\ptt filt_resolve_tac}, 104, 119
+  \item {\ptt filter} constant, 80
+  \item {\ptt filter_Cons} theorem, 81
+  \item {\ptt filter_Nil} theorem, 81
+  \item {\ptt Fin.consI} theorem, 47
+  \item {\ptt Fin.emptyI} theorem, 47
+  \item {\ptt Fin_induct} theorem, 47
+  \item {\ptt Fin_mono} theorem, 47
+  \item {\ptt Fin_subset} theorem, 47
+  \item {\ptt Fin_UnI} theorem, 47
+  \item {\ptt Fin_UnionI} theorem, 47
+  \item first-order logic, 4--21
+  \item {\ptt Fixedpt} theory, 40
+  \item {\ptt flat} constant, 48, 80
+  \item {\ptt flat_Cons} theorem, 81
+  \item {\ptt flat_def} theorem, 48
+  \item {\ptt flat_Nil} theorem, 81
+  \item flex-flex constraints, 98
+  \item {\ptt FOL} theory, 1, 4, 10, 121
+  \item {\ptt FOL_cs}, \bold{10}
+  \item {\ptt FOL_ss}, \bold{5}
+  \item {\ptt foldl} constant, 80
+  \item {\ptt foldl_Cons} theorem, 81
+  \item {\ptt foldl_Nil} theorem, 81
+  \item {\ptt form_rls}, \bold{119}
+  \item {\ptt formL_rls}, \bold{119}
+  \item {\ptt forms_of_seq}, \bold{103}
+  \item {\ptt foundation} theorem, 29
+  \item {\ptt fst} constant, 24, 31, 75, 111, 118
+  \item {\ptt fst_conv} theorem, 36, 75
+  \item {\ptt fst_def} theorem, 30, 116
+  \item {\ptt fun} type, 60
+  \item {\ptt fun_cong} theorem, 64
+  \item {\ptt fun_disjoint_apply1} theorem, 39, 55
+  \item {\ptt fun_disjoint_apply2} theorem, 39
+  \item {\ptt fun_disjoint_Un} theorem, 39, 57
+  \item {\ptt fun_empty} theorem, 39
+  \item {\ptt fun_extension} theorem, 38, 40
+  \item {\ptt fun_is_rel} theorem, 38
+  \item {\ptt fun_single} theorem, 39
+  \item function applications
+    \subitem in \CTT, 113
+    \subitem in \ZF, 24
+
+  \indexspace
+
+  \item {\ptt gfp_def} theorem, 44
+  \item {\ptt gfp_least} theorem, 44
+  \item {\ptt gfp_mono} theorem, 44
+  \item {\ptt gfp_subset} theorem, 44
+  \item {\ptt gfp_Tarski} theorem, 44
+  \item {\ptt gfp_upperbound} theorem, 44
+  \item {\ptt goalw}, 17
+
+  \indexspace
+
+  \item {\ptt hd} constant, 80
+  \item {\ptt hd_Cons} theorem, 81
+  \item higher-order logic, 58--97
+  \item {\ptt HOL} theory, 1, 58
+  \item {\sc hol} system, 58, 61
+  \item {\ptt HOL_cs}, \bold{75}
+  \item {\ptt HOL_quantifiers}, \bold{61}, 69
+  \item {\ptt HOL_ss}, \bold{74}
+  \item {\ptt HOLCF} theory, 1
+  \item {\ptt hyp_rew_tac}, \bold{120}
+  \item {\ptt hyp_subst_tac}, 5
+
+  \indexspace
+
+  \item {\ptt i} type, 23, 110
+  \item {\ptt id} constant, 45
+  \item {\ptt id_def} theorem, 45
+  \item {\ptt If} constant, 59
+  \item {\ptt if} constant, 24
+  \item {\ptt if_def} theorem, 16, 29, 62
+  \item {\ptt if_not_P} theorem, 34, 65
+  \item {\ptt if_P} theorem, 34, 65
+  \item {\ptt ifE} theorem, 18
+  \item {\ptt iff} theorem, 62, 63
+  \item {\ptt iff_def} theorem, 7, 101
+  \item {\ptt iff_impE} theorem, 8
+  \item {\ptt iffCE} theorem, 10, 65, 72
+  \item {\ptt iffD1} theorem, 8, 64
+  \item {\ptt iffD2} theorem, 8, 64
+  \item {\ptt iffE} theorem, 8, 64
+  \item {\ptt iffI} theorem, 8, 18, 64
+  \item {\ptt iffL} theorem, 102, 108
+  \item {\ptt iffR} theorem, 102
+  \item {\ptt ifI} theorem, 18
+  \item {\ptt IFOL} theory, 4
+  \item {\ptt IFOL_ss}, \bold{5}
+  \item {\ptt image_def} theorem, 30, 69
+  \item {\ptt imageE} theorem, 38, 72
+  \item {\ptt imageI} theorem, 38, 72
+  \item {\ptt imp_impE} theorem, 8, 13
+  \item {\ptt impCE} theorem, 10, 65
+  \item {\ptt impE} theorem, 8, 9, 64
+  \item {\ptt impI} theorem, 7, 62
+  \item {\ptt impL} theorem, 101
+  \item {\ptt impR} theorem, 101
+  \item {\ptt in} symbol, 26, 60
+  \item {\ptt ind} type, 77
+  \item {\ptt induct} theorem, 44
+  \item {\ptt inductive}, 91--94
+  \item {\ptt Inf} constant, 24, 28
+  \item {\ptt infinity} theorem, 30
+  \item {\ptt inj} constant, 45, 66
+  \item {\ptt inj_converse_inj} theorem, 45
+  \item {\ptt inj_def} theorem, 45, 69
+  \item {\ptt inj_Inl} theorem, 77
+  \item {\ptt inj_Inr} theorem, 77
+  \item {\ptt inj_inverseI} theorem, 72
+  \item {\ptt inj_onto} constant, 66, 72
+  \item {\ptt inj_onto_contraD} theorem, 72
+  \item {\ptt inj_onto_def} theorem, 69
+  \item {\ptt inj_onto_inverseI} theorem, 72
+  \item {\ptt inj_ontoD} theorem, 72
+  \item {\ptt inj_ontoI} theorem, 72
+  \item {\ptt inj_Suc} theorem, 78
+  \item {\ptt injD} theorem, 72
+  \item {\ptt injI} theorem, 72
+  \item {\ptt Inl} constant, 42, 77
+  \item {\ptt inl} constant, 111, 118, 126
+  \item {\ptt Inl_def} theorem, 42
+  \item {\ptt Inl_inject} theorem, 42
+  \item {\ptt Inl_neq_Inr} theorem, 42
+  \item {\ptt Inl_not_Inr} theorem, 77
+  \item {\ptt Inr} constant, 42, 77
+  \item {\ptt inr} constant, 111, 118
+  \item {\ptt Inr_def} theorem, 42
+  \item {\ptt Inr_inject} theorem, 42
+  \item {\ptt insert} constant, 66
+  \item {\ptt insert_def} theorem, 69
+  \item {\ptt insertE} theorem, 71
+  \item {\ptt insertI1} theorem, 71
+  \item {\ptt insertI2} theorem, 71
+  \item {\ptt INT} symbol, 25, 27, 66, 67, 69
+  \item {\ptt Int} symbol, 24, 66
+  \item {\ptt Int.best_tac}, \bold{9}
+  \item {\ptt Int.fast_tac}, \bold{9}, 12
+  \item {\ptt Int.inst_step_tac}, \bold{9}
+  \item {\ptt Int.safe_step_tac}, \bold{9}
+  \item {\ptt Int.safe_tac}, \bold{9}
+  \item {\ptt Int.step_tac}, \bold{9}
+  \item {\ptt Int_absorb} theorem, 41, 73
+  \item {\ptt Int_assoc} theorem, 41, 73
+  \item {\ptt Int_commute} theorem, 41, 73
+  \item {\ptt INT_D} theorem, 71
+  \item {\ptt Int_def} theorem, 29, 69
+  \item {\ptt INT_E} theorem, 33, 71
+  \item {\ptt Int_greatest} theorem, 35, 52, 53, 73
+  \item {\ptt INT_I} theorem, 33, 71
+  \item {\ptt Int_Inter_image} theorem, 73
+  \item {\ptt Int_lower1} theorem, 35, 52, 73
+  \item {\ptt Int_lower2} theorem, 35, 52, 73
+  \item {\ptt Int_Un_distrib} theorem, 41, 73
+  \item {\ptt Int_Union} theorem, 73
+  \item {\ptt Int_Union_RepFun} theorem, 41
+  \item {\ptt IntD1} theorem, 34, 71
+  \item {\ptt IntD2} theorem, 34, 71
+  \item {\ptt IntE} theorem, 34, 52, 71
+  \item {\ptt INTER} constant, 66
+  \item {\ptt Inter} constant, 24, 66
+  \item {\ptt INTER1} constant, 66
+  \item {\ptt INTER1_def} theorem, 69
+  \item {\ptt INTER_def} theorem, 69
+  \item {\ptt Inter_def} theorem, 29, 69
+  \item {\ptt Inter_greatest} theorem, 35, 73
+  \item {\ptt Inter_lower} theorem, 35, 73
+  \item {\ptt Inter_Un_distrib} theorem, 41, 73
+  \item {\ptt InterD} theorem, 33, 71
+  \item {\ptt InterE} theorem, 33, 71
+  \item {\ptt InterI} theorem, 31, 33, 71
+  \item {\ptt IntI} theorem, 34, 71
+  \item {\ptt intr_rls}, \bold{119}
+  \item {\ptt intr_tac}, \bold{120}, 128--130
+  \item {\ptt intrL_rls}, \bold{119}
+  \item {\ptt Inv} constant, 59, 72
+  \item {\ptt Inv_def} theorem, 62
+  \item {\ptt Inv_f_f} theorem, 72
+
+  \indexspace
+
+  \item {\ptt lam} symbol, 25, 27, 113
+  \item {\ptt lam_def} theorem, 30
+  \item {\ptt lam_type} theorem, 39
+  \item {\ptt Lambda} constant, 24, 28
+  \item {\ptt lambda} constant, 111, 113
+  \item $\lambda$-abstractions
+    \subitem in \CTT, 113
+    \subitem in \ZF, 25
+  \item {\ptt lamE} theorem, 39, 40
+  \item {\ptt lamI} theorem, 39, 40
+  \item {\ptt LCF} theory, 1
+  \item {\ptt le_cs}, \bold{22}
+  \item {\ptt left_comp_id} theorem, 45
+  \item {\ptt left_comp_inverse} theorem, 45
+  \item {\ptt left_inverse} theorem, 45
+  \item {\ptt length} constant, 48, 80
+  \item {\ptt length_Cons} theorem, 81
+  \item {\ptt length_def} theorem, 48
+  \item {\ptt length_Nil} theorem, 81
+  \item {\ptt less_induct} theorem, 79
+  \item {\ptt less_linear} theorem, 79
+  \item {\ptt less_not_refl} theorem, 79
+  \item {\ptt less_not_sym} theorem, 79
+  \item {\ptt less_trans} theorem, 79
+  \item {\ptt lessI} theorem, 79
+  \item {\ptt Let} constant, 23, 24, 59, 61
+  \item {\ptt let} symbol, 26, 60, 61
+  \item {\ptt Let_def} theorem, 23, 29, 61, 62
+  \item {\ptt lfp_def} theorem, 44
+  \item {\ptt lfp_greatest} theorem, 44
+  \item {\ptt lfp_lowerbound} theorem, 44
+  \item {\ptt lfp_mono} theorem, 44
+  \item {\ptt lfp_subset} theorem, 44
+  \item {\ptt lfp_Tarski} theorem, 44
+  \item {\ptt List} theory, 80, 82
+  \item {\ptt list} constant, 48
+  \item {\ptt list} type, 82, 95
+  \item {\ptt List.induct} theorem, 48
+  \item {\ptt list_all} constant, 80
+  \item {\ptt list_all_Cons} theorem, 81
+  \item {\ptt list_all_Nil} theorem, 81
+  \item {\ptt list_case} constant, 48
+  \item {\ptt list_mono} theorem, 48
+  \item {\ptt list_rec} constant, 48
+  \item {\ptt list_rec_Cons} theorem, 48
+  \item {\ptt list_rec_def} theorem, 48
+  \item {\ptt list_rec_Nil} theorem, 48
+  \item {\ptt LK} theory, 1, 98, 102
+  \item {\ptt LK_dup_pack}, \bold{104}, 106
+  \item {\ptt LK_pack}, \bold{104}
+  \item {\ptt LList} theory, 95
+  \item {\ptt logic} class, 4
+
+  \indexspace
+
+  \item {\ptt map} constant, 48, 80
+  \item {\ptt map_app_distrib} theorem, 48
+  \item {\ptt map_compose} theorem, 48
+  \item {\ptt map_Cons} theorem, 81
+  \item {\ptt map_def} theorem, 48
+  \item {\ptt map_flat} theorem, 48
+  \item {\ptt map_ident} theorem, 48
+  \item {\ptt map_Nil} theorem, 81
+  \item {\ptt map_type} theorem, 48
+  \item {\ptt max} constant, 58
+  \item {\ptt mem} symbol, 80
+  \item {\ptt mem_asym} theorem, 34, 35
+  \item {\ptt mem_Collect_eq} theorem, 69
+  \item {\ptt mem_Cons} theorem, 81
+  \item {\ptt mem_irrefl} theorem, 34
+  \item {\ptt mem_Nil} theorem, 81
+  \item {\ptt min} constant, 58
+  \item {\ptt minus} class, 58
+  \item {\ptt mod} symbol, 46, 78, 122
+  \item {\ptt mod_def} theorem, 46, 122
+  \item {\ptt mod_geq} theorem, 79
+  \item {\ptt mod_less} theorem, 79
+  \item {\ptt mod_quo_equality} theorem, 46
+  \item {\ptt Modal} theory, 1
+  \item {\ptt mono} constant, 58, 66
+  \item {\ptt mono_def} theorem, 69
+  \item {\ptt monoD} theorem, 72
+  \item {\ptt monoI} theorem, 72
+  \item {\ptt mp} theorem, 7, 62
+  \item {\ptt mp_tac}, \bold{9}, \bold{121}
+  \item {\ptt mult_0} theorem, 46
+  \item {\ptt mult_assoc} theorem, 46, 122
+  \item {\ptt mult_commute} theorem, 46, 122
+  \item {\ptt mult_def} theorem, 46, 79, 122
+  \item {\ptt mult_Suc} theorem, 79
+  \item {\ptt mult_succ} theorem, 46
+  \item {\ptt mult_type} theorem, 46
+  \item {\ptt mult_typing} theorem, 122
+  \item {\ptt multC0} theorem, 122
+  \item {\ptt multC_succ} theorem, 122
+
+  \indexspace
+
+  \item {\ptt N} constant, 111
+  \item {\ptt n_not_Suc_n} theorem, 78
+  \item {\ptt Nat} theory, 43, 77
+  \item {\ptt nat} constant, 46
+  \item {\ptt nat} type, 77
+  \item {\ptt nat_0I} theorem, 46
+  \item {\ptt nat_case} constant, 46, 78
+  \item {\ptt nat_case_0} theorem, 46, 79
+  \item {\ptt nat_case_def} theorem, 46
+  \item {\ptt nat_case_Suc} theorem, 79
+  \item {\ptt nat_case_succ} theorem, 46
+  \item {\ptt nat_def} theorem, 46
+  \item {\ptt nat_ind_tac}, 77
+  \item {\ptt nat_induct} theorem, 46, 78
+  \item {\ptt nat_rec} constant, 78
+  \item {\ptt nat_rec_0} theorem, 79
+  \item {\ptt nat_rec_Suc} theorem, 79
+  \item {\ptt nat_succI} theorem, 46
+  \item {\ptt NC0} theorem, 115
+  \item {\ptt NC_succ} theorem, 115
+  \item {\ptt NE} theorem, 115, 116, 124
+  \item {\ptt NEL} theorem, 115
+  \item {\ptt NF} theorem, 115, 124
+  \item {\ptt NI0} theorem, 115
+  \item {\ptt NI_succ} theorem, 115
+  \item {\ptt NI_succL} theorem, 115
+  \item {\ptt Nil_Cons_iff} theorem, 48
+  \item {\ptt NilI} theorem, 48
+  \item {\ptt NIO} theorem, 124
+  \item {\ptt Not} constant, 6, 99
+  \item {\ptt not} constant, 59
+  \item {\ptt not_def} theorem, 7, 42, 62
+  \item {\ptt not_impE} theorem, 8
+  \item {\ptt not_less0} theorem, 79
+  \item {\ptt not_sym} theorem, 64
+  \item {\ptt notE} theorem, 8, 9, 64
+  \item {\ptt notI} theorem, 8, 64
+  \item {\ptt notL} theorem, 101
+  \item {\ptt notnotD} theorem, 10, 65
+  \item {\ptt notR} theorem, 101
+  \item {\ptt null} constant, 80
+  \item {\ptt null_Cons} theorem, 81
+  \item {\ptt null_Nil} theorem, 81
+
+  \indexspace
+
+  \item {\ptt O} symbol, 45
+  \item {\ptt o} symbol, 59, 72
+  \item {\ptt o} type, 4, 98
+  \item {\ptt o_def} theorem, 62
+  \item {\ptt of} symbol, 61
+  \item {\ptt or_def} theorem, 42, 62
+  \item {\ptt ord} class, 58, 77
+
+  \indexspace
+
+  \item {\ptt pack} ML type, 104
+  \item {\ptt Pair} constant, 24, 25, 75
+  \item {\ptt pair} constant, 111
+  \item {\ptt Pair_def} theorem, 30
+  \item {\ptt Pair_eq} theorem, 75
+  \item {\ptt Pair_inject} theorem, 36, 75
+  \item {\ptt Pair_inject1} theorem, 36
+  \item {\ptt Pair_inject2} theorem, 36
+  \item {\ptt Pair_neq_0} theorem, 36
+  \item {\ptt PairE} theorem, 75
+  \item {\ptt pairing} theorem, 33
+  \item {\ptt pc_tac}, \bold{105}, \bold{121}, 127--129
+  \item {\ptt Perm} theory, 43
+  \item {\ptt Pi} constant, 24, 27, 40
+  \item {\ptt Pi_def} theorem, 30
+  \item {\ptt Pi_type} theorem, 38, 40
+  \item {\ptt plus} class, 58
+  \item {\ptt PlusC_inl} theorem, 117
+  \item {\ptt PlusC_inr} theorem, 117
+  \item {\ptt PlusE} theorem, 117, 121, 126
+  \item {\ptt PlusEL} theorem, 117
+  \item {\ptt PlusF} theorem, 117
+  \item {\ptt PlusFL} theorem, 117
+  \item {\ptt PlusI_inl} theorem, 117, 126
+  \item {\ptt PlusI_inlL} theorem, 117
+  \item {\ptt PlusI_inr} theorem, 117
+  \item {\ptt PlusI_inrL} theorem, 117
+  \item {\ptt Pow} constant, 24, 66
+  \item {\ptt Pow_def} theorem, 69
+  \item {\ptt Pow_iff} theorem, 29
+  \item {\ptt Pow_mono} theorem, 51
+  \item {\ptt PowD} theorem, 32, 53, 71
+  \item {\ptt PowI} theorem, 32, 53, 71
+  \item primitive recursion, 90--91
+  \item {\ptt primrec}, 90--91
+  \item {\ptt PrimReplace} constant, 24, 28
+  \item priorities, 2
+  \item {\ptt PROD} symbol, 25, 27, 112, 113
+  \item {\ptt Prod} constant, 111
+  \item {\ptt Prod} theory, 75
+  \item {\ptt ProdC} theorem, 115, 131
+  \item {\ptt ProdC2} theorem, 115
+  \item {\ptt ProdE} theorem, 115, 129, 130, 132
+  \item {\ptt ProdEL} theorem, 115
+  \item {\ptt ProdF} theorem, 115
+  \item {\ptt ProdFL} theorem, 115
+  \item {\ptt ProdI} theorem, 115, 121, 124
+  \item {\ptt ProdIL} theorem, 115
+  \item {\ptt prop_cs}, \bold{10}, \bold{75}
+  \item {\ptt prop_pack}, \bold{104}
+
+  \indexspace
+
+  \item {\ptt qcase_def} theorem, 43
+  \item {\ptt qconverse} constant, 40
+  \item {\ptt qconverse_def} theorem, 43
+  \item {\ptt qfsplit_def} theorem, 43
+  \item {\ptt QInl_def} theorem, 43
+  \item {\ptt QInr_def} theorem, 43
+  \item {\ptt QPair} theory, 40
+  \item {\ptt QPair_def} theorem, 43
+  \item {\ptt QSigma} constant, 40
+  \item {\ptt QSigma_def} theorem, 43
+  \item {\ptt qsplit} constant, 40
+  \item {\ptt qsplit_def} theorem, 43
+  \item {\ptt qsum_def} theorem, 43
+  \item {\ptt QUniv} theory, 43
+
+  \indexspace
+
+  \item {\ptt range} constant, 24, 66, 96
+  \item {\ptt range_def} theorem, 30, 69
+  \item {\ptt range_of_fun} theorem, 38, 40
+  \item {\ptt range_subset} theorem, 37
+  \item {\ptt range_type} theorem, 38
+  \item {\ptt rangeE} theorem, 37, 72, 96
+  \item {\ptt rangeI} theorem, 37, 72
+  \item {\ptt rank} constant, 47
+  \item {\ptt rank_ss}, \bold{22}
+  \item {\ptt rec} constant, 46, 111, 116
+  \item {\ptt rec_0} theorem, 46
+  \item {\ptt rec_def} theorem, 46
+  \item {\ptt rec_succ} theorem, 46
+  \item {\ptt red_if_equal} theorem, 114
+  \item {\ptt Reduce} constant, 111, 116, 120
+  \item {\ptt refl} theorem, 7, 62, 101
+  \item {\ptt refl_elem} theorem, 114, 119
+  \item {\ptt refl_red} theorem, 114
+  \item {\ptt refl_type} theorem, 114, 119
+  \item {\ptt REPEAT_FIRST}, 119
+  \item {\ptt repeat_goal_tac}, \bold{105}
+  \item {\ptt RepFun} constant, 24, 27, 28, 31
+  \item {\ptt RepFun_def} theorem, 29
+  \item {\ptt RepFunE} theorem, 33
+  \item {\ptt RepFunI} theorem, 33
+  \item {\ptt Replace} constant, 24, 27, 28, 31
+  \item {\ptt Replace_def} theorem, 29
+  \item {\ptt replace_type} theorem, 118, 131
+  \item {\ptt ReplaceE} theorem, 33
+  \item {\ptt ReplaceI} theorem, 33
+  \item {\ptt replacement} theorem, 29
+  \item {\ptt reresolve_tac}, \bold{105}
+  \item {\ptt res_inst_tac}, 63
+  \item {\ptt restrict} constant, 24, 31
+  \item {\ptt restrict} theorem, 38
+  \item {\ptt restrict_bij} theorem, 45
+  \item {\ptt restrict_def} theorem, 30
+  \item {\ptt restrict_type} theorem, 38
+  \item {\ptt rev} constant, 48, 80
+  \item {\ptt rev_Cons} theorem, 81
+  \item {\ptt rev_def} theorem, 48
+  \item {\ptt rev_Nil} theorem, 81
+  \item {\ptt rew_tac}, 17, \bold{120}
+  \item {\ptt rewrite_rule}, 18
+  \item {\ptt right_comp_id} theorem, 45
+  \item {\ptt right_comp_inverse} theorem, 45
+  \item {\ptt right_inverse} theorem, 45
+  \item {\ptt RL}, 126
+  \item {\ptt RS}, 130, 132
+
+  \indexspace
+
+  \item {\ptt safe_goal_tac}, \bold{106}
+  \item {\ptt safe_tac}, \bold{121}
+  \item {\ptt safestep_tac}, \bold{121}
+  \item search
+    \subitem best-first, 97
+  \item {\ptt select_equality} theorem, 63, 65
+  \item {\ptt selectI} theorem, 62, 63
+  \item {\ptt separation} theorem, 33
+  \item {\ptt Seqof} constant, 99
+  \item sequent calculus, 98--109
+  \item {\ptt Set} theory, 68, 69
+  \item {\ptt set} type, 68
+  \item set theory, 22--57
+  \item {\ptt set_cs}, \bold{75}, 97
+  \item {\ptt set_diff_def} theorem, 69
+  \item {\ptt show_sorts}, 63
+  \item {\ptt show_types}, 63
+  \item {\ptt Sigma} constant, 24, 27, 28, 36, 75
+  \item {\ptt Sigma_def} theorem, 30, 75
+  \item {\ptt SigmaE} theorem, 36, 75
+  \item {\ptt SigmaE2} theorem, 36
+  \item {\ptt SigmaI} theorem, 36, 75
+  \item simplification
+    \subitem of conjunctions, 74
+  \item {\ptt singletonE} theorem, 34
+  \item {\ptt singletonI} theorem, 34
+  \item {\ptt snd} constant, 24, 31, 75, 111, 118
+  \item {\ptt snd_conv} theorem, 36, 75
+  \item {\ptt snd_def} theorem, 30, 116
+  \item {\ptt sobj} type, 100
+  \item {\ptt spec} theorem, 7, 65
+  \item {\ptt split} constant, 24, 31, 75, 111, 126
+  \item {\ptt split} theorem, 36, 75
+  \item {\ptt split_all_tac}, \bold{76}
+  \item {\ptt split_def} theorem, 30
+  \item {\ptt ssubst} theorem, 8, 63, 64
+  \item {\ptt stac}, \bold{74}
+  \item {\ptt step_tac}, 21, \bold{106}, \bold{121}
+  \item {\ptt strip_tac}, \bold{63}
+  \item {\ptt subset_def} theorem, 29, 69
+  \item {\ptt subset_refl} theorem, 32, 70
+  \item {\ptt subset_trans} theorem, 32, 70
+  \item {\ptt subsetCE} theorem, 32, 70, 72
+  \item {\ptt subsetD} theorem, 32, 55, 70, 72
+  \item {\ptt subsetI} theorem, 32, 52, 54, 70
+  \item {\ptt subst} theorem, 7, 62
+  \item {\ptt subst_elem} theorem, 114
+  \item {\ptt subst_elemL} theorem, 114
+  \item {\ptt subst_eqtyparg} theorem, 118, 131
+  \item {\ptt subst_prodE} theorem, 118
+  \item {\ptt subst_type} theorem, 114
+  \item {\ptt subst_typeL} theorem, 114
+  \item {\ptt Suc} constant, 78
+  \item {\ptt Suc_less_eq} theorem, 79
+  \item {\ptt Suc_not_Zero} theorem, 78
+  \item {\ptt succ} constant, 24, 28, 111
+  \item {\ptt succ_def} theorem, 30
+  \item {\ptt succ_inject} theorem, 34
+  \item {\ptt succ_neq_0} theorem, 34
+  \item {\ptt succCI} theorem, 34
+  \item {\ptt succE} theorem, 34
+  \item {\ptt succI1} theorem, 34
+  \item {\ptt succI2} theorem, 34
+  \item {\ptt SUM} symbol, 25, 27, 112, 113
+  \item {\ptt Sum} constant, 111
+  \item {\ptt Sum} theory, 40, 76
+  \item {\ptt sum_case} constant, 77
+  \item {\ptt sum_case_Inl} theorem, 77
+  \item {\ptt sum_case_Inr} theorem, 77
+  \item {\ptt sum_def} theorem, 42
+  \item {\ptt sum_InlI} theorem, 42
+  \item {\ptt sum_InrI} theorem, 42
+  \item {\ptt SUM_Int_distrib1} theorem, 41
+  \item {\ptt SUM_Int_distrib2} theorem, 41
+  \item {\ptt SUM_Un_distrib1} theorem, 41
+  \item {\ptt SUM_Un_distrib2} theorem, 41
+  \item {\ptt SumC} theorem, 116
+  \item {\ptt SumE} theorem, 116, 121, 126
+  \item {\ptt sumE} theorem, 77
+  \item {\ptt sumE2} theorem, 42
+  \item {\ptt SumE_fst} theorem, 118, 130, 132
+  \item {\ptt SumE_snd} theorem, 118, 132
+  \item {\ptt SumEL} theorem, 116
+  \item {\ptt SumF} theorem, 116
+  \item {\ptt SumFL} theorem, 116
+  \item {\ptt SumI} theorem, 116, 127
+  \item {\ptt SumIL} theorem, 116
+  \item {\ptt SumIL2} theorem, 118
+  \item {\ptt surj} constant, 45, 66, 72
+  \item {\ptt surj_def} theorem, 45, 69
+  \item {\ptt surjective_pairing} theorem, 75
+  \item {\ptt surjective_sum} theorem, 77
+  \item {\ptt swap} theorem, 10, 65
+  \item {\ptt swap_res_tac}, 15, 97
+  \item {\ptt sym} theorem, 8, 64, 101
+  \item {\ptt sym_elem} theorem, 114
+  \item {\ptt sym_type} theorem, 114
+  \item {\ptt symL} theorem, 102
+
+  \indexspace
+
+  \item {\ptt T} constant, 111
+  \item {\ptt t} type, 110
+  \item {\ptt TC} theorem, 117
+  \item {\ptt TE} theorem, 117
+  \item {\ptt TEL} theorem, 117
+  \item {\ptt term} class, 4, 58, 60, 63, 98
+  \item {\ptt test_assume_tac}, \bold{120}
+  \item {\ptt TF} theorem, 117
+  \item {\ptt THE} symbol, 25, 27, 35, 99
+  \item {\ptt The} constant, 24, 27, 28, 99
+  \item {\ptt The} theorem, 101
+  \item {\ptt the_def} theorem, 29
+  \item {\ptt the_equality} theorem, 34, 35
+  \item {\ptt theI} theorem, 34, 35
+  \item {\ptt thinL} theorem, 101
+  \item {\ptt thinR} theorem, 101
+  \item {\ptt TI} theorem, 117
+  \item {\ptt times} class, 58
+  \item {\ptt tl} constant, 80
+  \item {\ptt tl_Cons} theorem, 81
+  \item tracing
+    \subitem of unification, 63
+  \item {\ptt trans} theorem, 8, 64, 101
+  \item {\ptt trans_elem} theorem, 114
+  \item {\ptt trans_red} theorem, 114
+  \item {\ptt trans_type} theorem, 114
+  \item {\ptt True} constant, 6, 59, 99
+  \item {\ptt True_def} theorem, 7, 62, 101
+  \item {\ptt True_or_False} theorem, 62, 63
+  \item {\ptt TrueI} theorem, 8, 64
+  \item {\ptt Trueprop} constant, 6, 59, 99
+  \item {\ptt TrueR} theorem, 102
+  \item {\ptt tt} constant, 111
+  \item {\ptt ttl} constant, 80
+  \item {\ptt ttl_Cons} theorem, 81
+  \item {\ptt ttl_Nil} theorem, 81
+  \item {\ptt Type} constant, 111
+  \item type definition, \bold{82}
+  \item {\ptt typechk_tac}, \bold{120}, 124, 127, 132
+
+  \indexspace
+
+  \item {\ptt UN} symbol, 25, 27, 66, 67, 69
+  \item {\ptt Un} symbol, 24, 66
+  \item {\ptt Un1} theorem, 72
+  \item {\ptt Un2} theorem, 72
+  \item {\ptt Un_absorb} theorem, 41, 73
+  \item {\ptt Un_assoc} theorem, 41, 73
+  \item {\ptt Un_commute} theorem, 41, 73
+  \item {\ptt Un_def} theorem, 29, 69
+  \item {\ptt UN_E} theorem, 33, 71
+  \item {\ptt UN_I} theorem, 33, 71
+  \item {\ptt Un_Int_distrib} theorem, 41, 73
+  \item {\ptt Un_Inter} theorem, 73
+  \item {\ptt Un_Inter_RepFun} theorem, 41
+  \item {\ptt Un_least} theorem, 35, 73
+  \item {\ptt Un_Union_image} theorem, 73
+  \item {\ptt Un_upper1} theorem, 35, 73
+  \item {\ptt Un_upper2} theorem, 35, 73
+  \item {\ptt UnCI} theorem, 34, 35, 71, 72
+  \item {\ptt UnE} theorem, 34, 71
+  \item {\ptt UnI1} theorem, 34, 35, 56, 71
+  \item {\ptt UnI2} theorem, 34, 35, 71
+  \item unification
+    \subitem incompleteness of, 63
+  \item {\ptt Unify.trace_types}, 63
+  \item {\ptt UNION} constant, 66
+  \item {\ptt Union} constant, 24, 66
+  \item {\ptt UNION1} constant, 66
+  \item {\ptt UNION1_def} theorem, 69
+  \item {\ptt UNION_def} theorem, 69
+  \item {\ptt Union_def} theorem, 69
+  \item {\ptt Union_iff} theorem, 29
+  \item {\ptt Union_least} theorem, 35, 73
+  \item {\ptt Union_Un_distrib} theorem, 41, 73
+  \item {\ptt Union_upper} theorem, 35, 73
+  \item {\ptt UnionE} theorem, 33, 54, 71
+  \item {\ptt UnionI} theorem, 33, 54, 71
+  \item {\ptt unit_eq} theorem, 76
+  \item {\ptt Univ} theory, 43
+  \item {\ptt Upair} constant, 23, 24, 28
+  \item {\ptt Upair_def} theorem, 29
+  \item {\ptt UpairE} theorem, 33
+  \item {\ptt UpairI1} theorem, 33
+  \item {\ptt UpairI2} theorem, 33
+
+  \indexspace
+
+  \item {\ptt vimage_def} theorem, 30
+  \item {\ptt vimageE} theorem, 38
+  \item {\ptt vimageI} theorem, 38
+
+  \indexspace
+
+  \item {\ptt when} constant, 111, 118, 126
+
+  \indexspace
+
+  \item {\ptt xor_def} theorem, 42
+
+  \indexspace
+
+  \item {\ptt zero_less_Suc} theorem, 79
+  \item {\ptt zero_ne_succ} theorem, 115, 116
+  \item {\ptt ZF} theory, 1, 22, 58
+  \item {\ptt ZF_cs}, \bold{22}
+  \item {\ptt ZF_ss}, \bold{22}
+
+\end{theindex}

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