1signature Drule = 2sig 3 include Abbrev 4 5 val ETA_CONV : conv 6 val RIGHT_ETA : thm -> thm 7 val EXT : thm -> thm 8 val MK_ABS : thm -> thm 9 val MK_EXISTS : thm -> thm 10 val LIST_MK_EXISTS : term list -> thm -> thm 11 val SIMPLE_EXISTS : term -> thm -> thm 12 val SIMPLE_CHOOSE : term -> thm -> thm 13 val EXISTS_LEFT : term list -> thm -> thm 14 val EXISTS_LEFT1 : term -> thm -> thm 15 val EQT_INTRO : thm -> thm 16 val GSUBS : ((term,term)subst -> term -> term) 17 -> thm list -> thm -> thm 18 val SUBST_CONV : (term,thm)subst -> term -> conv 19 val ADD_ASSUM : term -> thm -> thm 20 val IMP_TRANS : thm -> thm -> thm 21 val IMP_ANTISYM_RULE : thm -> thm -> thm 22 val CONTR : term -> thm -> thm 23 val UNDISCH : thm -> thm 24 val UNDISCH_TM : thm -> term * thm 25 val UNDISCH_SPLIT : thm -> thm 26 val EQT_ELIM : thm -> thm 27 val SPECL : term list -> thm -> thm 28 val SELECT_INTRO : thm -> thm 29 val SELECT_ELIM : thm -> term * thm -> thm 30 val SELECT_RULE : thm -> thm 31 val SPEC_VAR : thm -> term * thm 32 val SPEC_UNDISCH_EXL : thm -> thm 33 val FORALL_EQ : term -> thm -> thm 34 val EXISTS_EQ : term -> thm -> thm 35 val SELECT_EQ : term -> thm -> thm 36 val SUBS : thm list -> thm -> thm 37 val SUBS_OCCS : (int list * thm) list -> thm -> thm 38 val RIGHT_BETA : thm -> thm 39 val LIST_BETA_CONV : conv 40 val RIGHT_LIST_BETA : thm -> thm 41 val ASSUME_CONJS : term -> thm 42 val CONJUNCTS_AC : term * term -> thm 43 val DISJUNCTS_AC : term * term -> thm 44 val CONJ_DISCH : term -> thm -> thm 45 val CONJ_DISCHL : term list -> thm -> thm 46 val NEG_DISCH : term -> thm -> thm 47 val NOT_EQ_SYM : thm -> thm 48 val EQF_INTRO : thm -> thm 49 val EQF_ELIM : thm -> thm 50 val ISPEC : term -> thm -> thm 51 val ISPECL : term list -> thm -> thm 52 val GEN_ALL : thm -> thm 53 val DISCH_ALL : thm -> thm 54 val UNDISCH_ALL : thm -> thm 55 val SPEC_ALL : thm -> thm 56 val PROVE_HYP : thm -> thm -> thm 57 val REORDER_ANTS_MOD : (term list -> term list) -> (thm -> thm) -> thm -> thm 58 val REORDER_ANTS : (term list -> term list) -> thm -> thm 59 val MODIFY_CONS : (thm -> thm) -> thm -> thm 60 val CONJ_PAIR : thm -> thm * thm 61 val LIST_CONJ : thm list -> thm 62 val CONJ_LIST : int -> thm -> thm list 63 val CONJUNCTS : thm -> thm list 64 val BODY_CONJUNCTS : thm -> thm list 65 val IMP_CANON : thm -> thm list 66 val MP_GENEQ_CANON : bool list -> thm -> thm 67 val MP_CANON : thm -> thm 68 val MP_LEQ_CANON : thm -> thm 69 val MP_REQ_CANON : thm -> thm 70 val LIST_MP : thm list -> thm -> thm 71 val CONTRAPOS : thm -> thm 72 val DISJ_IMP : thm -> thm 73 val IMP_ELIM : thm -> thm 74 val DISJ_CASES_UNION : thm -> thm -> thm -> thm 75 val DISJ_CASESL : thm -> thm list -> thm 76 val ALPHA_CONV : term -> conv 77 val GEN_ALPHA_CONV : term -> conv 78 val IMP_CONJ : thm -> thm -> thm 79 val EXISTS_IMP : term -> thm -> thm 80 val INST_TY_TERM : (term,term)subst * (hol_type,hol_type)subst 81 -> thm -> thm 82 val INST_TT_HYPS : (term,term)subst * (hol_type,hol_type)subst 83 -> thm -> thm * term list 84 val GEN_TYVARIFY : thm -> thm 85 val FULL_GEN_TYVARIFY: thm -> thm 86 val GSPEC : thm -> thm 87 88 val PART_MATCH : (term -> term) -> thm -> term -> thm 89 val PART_MATCH' : (term -> term) -> thm -> term -> thm 90 val PART_MATCH_A : (term -> term) -> thm -> term -> thm 91 val MATCH_MP : thm -> thm -> thm 92 val BETA_VAR : term -> term -> term -> thm 93 val HO_PART_MATCH : (term -> term) -> thm -> term -> thm 94 val HO_MATCH_MP : thm -> thm -> thm 95 val RES_CANON : thm -> thm list 96 val IRULE_CANON : thm -> thm 97 98 val prove_rep_fn_one_one : thm -> thm 99 val prove_rep_fn_onto : thm -> thm 100 val prove_abs_fn_onto : thm -> thm 101 val prove_abs_fn_one_one : thm -> thm 102 103 val define_new_type_bijections 104 : {name:string, ABS:string, REP:string, tyax:thm} -> thm 105 106 val MK_AC_LCOMM : thm * thm -> thm * thm * thm 107 108 val underAIs : (thm -> thm) -> thm -> thm 109 val iffLR : thm -> thm 110 val iffRL : thm -> thm 111 val cj : int -> thm -> thm 112 val pp : thmpos_dtype.match_position -> thm -> thm 113 114 115end 116