1signature Tactic = 2sig 3 include Abbrev 4 datatype match_position = datatype thmpos_dtype.match_position 5 6 val ACCEPT_TAC : thm_tactic 7 val DISCARD_TAC : thm_tactic 8 val CONTR_TAC : thm_tactic 9 val CCONTR_TAC : tactic 10 val ASSUME_TAC : thm_tactic 11 val assume_tac : thm_tactic 12 val FREEZE_THEN : thm_tactical 13 val CONJ_TAC : tactic 14 val conj_tac : tactic 15 val CONJ_ASM1_TAC : tactic 16 val conj_asm1_tac : tactic 17 val CONJ_ASM2_TAC : tactic 18 val conj_asm2_tac : tactic 19 val DISJ1_TAC : tactic 20 val disj1_tac : tactic 21 val DISJ2_TAC : tactic 22 val disj2_tac : tactic 23 val MP_TAC : thm_tactic 24 val mp_tac : thm_tactic 25 val EQ_TAC : tactic 26 val eq_tac : tactic 27 val X_GEN_TAC : term -> tactic 28 val GEN_TAC : tactic 29 val gen_tac : tactic 30 val SPEC_TAC : term * term -> tactic 31 val ID_SPEC_TAC : term -> tactic 32 val EXISTS_TAC : term -> tactic 33 val exists_tac : term -> tactic 34 val ID_EX_TAC : tactic 35 val GSUBST_TAC : ((term,term) Lib.subst -> term -> term) 36 -> thm list -> tactic 37 val SUBST_TAC : thm list -> tactic 38 val SUBST_OCCS_TAC : (int list * thm) list -> tactic 39 val SUBST1_TAC : thm -> tactic 40 val RULE_ASSUM_TAC : (thm -> thm) -> tactic 41 val rule_assum_tac : (thm -> thm) -> tactic 42 val RULE_L_ASSUM_TAC : (thm -> thm list) -> tactic 43 val SUBST_ALL_TAC : thm -> tactic 44 val CHECK_ASSUME_TAC : thm_tactic 45 val STRIP_ASSUME_TAC : thm_tactic 46 val strip_assume_tac : thm_tactic 47 val STRUCT_CASES_TAC : thm_tactic 48 val FULL_STRUCT_CASES_TAC : thm_tactic 49 val GEN_COND_CASES_TAC : (term -> bool) -> tactic 50 val COND_CASES_TAC : tactic 51 val IF_CASES_TAC : tactic 52 val BOOL_CASES_TAC : term -> tactic 53 val STRIP_GOAL_THEN : thm_tactic -> tactic 54 val FILTER_GEN_TAC : term -> tactic 55 val FILTER_DISCH_THEN : thm_tactic -> term -> tactic 56 val FILTER_STRIP_THEN : thm_tactic -> term -> tactic 57 val DISCH_TAC : tactic 58 val disch_tac : tactic 59 val DISJ_CASES_TAC : thm_tactic 60 val CHOOSE_TAC : thm_tactic 61 val X_CHOOSE_TAC : term -> thm_tactic 62 val STRIP_TAC : tactic 63 val strip_tac : tactic 64 val FILTER_DISCH_TAC : term -> tactic 65 val FILTER_STRIP_TAC : term -> tactic 66 val ASM_CASES_TAC : term -> tactic 67 val REFL_TAC : tactic 68 val UNDISCH_TAC : term -> tactic 69 val AP_TERM_TAC : tactic 70 val AP_THM_TAC : tactic 71 val MK_COMB_TAC : tactic 72 val BINOP_TAC : tactic 73 val ABS_TAC : tactic 74 val NTAC : int -> tactic -> tactic 75 val ntac : int -> tactic -> tactic 76 val WEAKEN_TAC : (term -> bool) -> tactic 77 val MATCH_ACCEPT_TAC : thm -> tactic 78 val MATCH_MP_TAC : thm -> tactic 79 val match_mp_tac : thm -> tactic 80 val prim_irule : thm -> tactic 81 val irule : thm -> tactic 82 val irule_at : match_position -> thm -> tactic 83 val IRULE_TAC : thm -> tactic 84 val impl_tac : tactic 85 val impl_keep_tac : tactic 86 val HO_MATCH_ACCEPT_TAC : thm -> tactic 87 val HO_BACKCHAIN_TAC : thm -> tactic 88 val HO_MATCH_MP_TAC : thm -> tactic 89 val ho_match_mp_tac : thm -> tactic 90 val IMP_RES_TAC : thm -> tactic 91 val imp_res_tac : thm -> tactic 92 val RES_TAC : tactic 93 val res_tac : tactic 94 val provehyp : thm_tactic 95 val via : term * tactic -> tactic 96 val CONV_TAC : conv -> tactic 97 val BETA_TAC : tactic 98 val KNOW_TAC : term -> tactic 99 val SUFF_TAC : term -> tactic 100 val suff_tac : term -> tactic 101 102 103 val eliminable : term -> bool 104 val VSUBST_TAC : thm -> tactic 105 106 val DEEP_INTROk_TAC : thm -> tactic -> tactic 107 val DEEP_INTRO_TAC : thm -> tactic 108 109 val SELECT_ELIM_TAC : tactic 110 val HINT_EXISTS_TAC : tactic 111 val part_match_exists_tac : (term -> term) -> term -> tactic 112 113 val drule : thm_tactic 114 val dxrule : thm_tactic 115 val rev_drule : thm_tactic 116 val rev_dxrule : thm_tactic 117 118 val drule_at : match_position -> thm_tactic 119 val dxrule_at : match_position -> thm_tactic 120 val rev_drule_at : match_position -> thm_tactic 121 val rev_dxrule_at : match_position -> thm_tactic 122 123 val drule_then : thm_tactic -> thm_tactic 124 val dxrule_then : thm_tactic -> thm_tactic 125 val rev_drule_then : thm_tactic -> thm_tactic 126 val rev_dxrule_then : thm_tactic -> thm_tactic 127 128 val drule_at_then : match_position -> thm_tactic -> thm_tactic 129 val dxrule_at_then : match_position -> thm_tactic -> thm_tactic 130 val rev_drule_at_then : match_position -> thm_tactic -> thm_tactic 131 val rev_dxrule_at_then : match_position -> thm_tactic -> thm_tactic 132 133 134 val drule_all : thm_tactic 135 val dxrule_all : thm_tactic 136 val drule_all_then : thm_tactic -> thm_tactic 137 val dxrule_all_then : thm_tactic -> thm_tactic 138 139 val rev_drule_all : thm_tactic 140 val rev_dxrule_all : thm_tactic 141 val rev_drule_all_then : thm_tactic -> thm_tactic 142 val rev_dxrule_all_then : thm_tactic -> thm_tactic 143 144 145 val mp_then : match_position -> thm_tactic -> thm -> thm -> tactic 146 val resolve_then : match_position -> thm_tactic -> thm -> thm -> tactic 147 148end 149