1signature schneiderUtils = 2 sig 3 type term = Term.term 4 type thm = Thm.thm 5 type goal = Abbrev.goal 6 type conv = Abbrev.conv 7 type tactic = Abbrev.tactic 8 9 val APPLY_ASM_TAC : int -> tactic -> tactic 10 val ASM_LIST_TAC : int list 11 -> (thm list -> term list * 'a -> 'b) 12 -> term list * 'a -> 'b 13 val ASM_TAC : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b 14 val BOOL_VAR_ELIM_CONV : term -> term -> thm 15 val BOOL_VAR_ELIM_TAC : term -> tactic 16 val COND_FUN_EXT_CONV : term -> thm 17 val COND_FUN_EXT_TAC : tactic 18 val COPY_ASM_NO : int -> tactic 19 val FORALL_IN_CONV : conv 20 val FORALL_UNFREE_CONV : term -> thm 21 val LEFT_CONJ_TAC : tactic 22 val LEFT_DISJ_TAC : tactic 23 val LEFT_EXISTS_TAC : tactic 24 val LEFT_FORALL_TAC : term -> tactic 25 val LEFT_LEMMA_DISJ_CASES_TAC : thm -> tactic 26 val LEFT_NO_EXISTS_TAC : int -> tactic 27 val LEFT_NO_FORALL_TAC : int -> term -> tactic 28 val MP2_TAC : thm -> goal -> (term list * term) list * (thm list -> thm) 29 val MY_MP_TAC : term -> goal -> (term list * term) list * (thm list -> thm) 30 val POP_NO_ASSUM : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b 31 val POP_NO_TAC : int -> tactic 32 val PROP_TAC : tactic 33 val REW_PROP_TAC : tactic 34 val RIGHT_CONJ_TAC : tactic 35 val RIGHT_DISJ_TAC : tactic 36 val RIGHT_LEMMA_DISJ_CASES_TAC : thm -> tactic 37 val REWRITE1_TAC : thm -> tactic 38 val SELECT_EXISTS_TAC : term -> tactic 39 val SELECT_UNIQUE_RULE : term -> thm -> thm -> thm 40 val SELECT_UNIQUE_TAC : tactic 41 val SELECT_UNIQUE_THM : thm 42 val TAC_CONV : tactic -> term -> thm 43 val UNDISCH_ALL_TAC : tactic 44 val UNDISCH_HD_TAC : tactic 45 val UNDISCH_NO_TAC : int -> tactic 46 val delete : int -> 'a list -> 'a list 47 val elem : int -> 'a list -> 'a 48 val prove_thm : string * term * tactic -> thm 49 end 50