1signature Thm = 2sig 3 4 include FinalThm where type hol_type = Type.hol_type 5 and type term = Term.term 6 and type tag = Tag.tag 7 8 datatype proof = 9 Axiom_prf 10 | ABS_prf of term * thm 11 | ALPHA_prf of term * term 12 | AP_TERM_prf of term * thm 13 | AP_THM_prf of thm * term 14 | ASSUME_prf of term 15 | BETA_CONV_prf of term 16 | CCONTR_prf of term * thm 17 | CHOOSE_prf of term * thm * thm 18 | CONJ_prf of thm * thm 19 | CONJUNCT1_prf of thm 20 | CONJUNCT2_prf of thm 21 | DISCH_prf of term * thm 22 | DISJ_CASES_prf of thm * thm * thm 23 | DISJ1_prf of thm * term 24 | DISJ2_prf of term * thm 25 | EQ_IMP_RULE1_prf of thm 26 | EQ_IMP_RULE2_prf of thm 27 | EQ_MP_prf of thm * thm 28 | EXISTS_prf of term * term * thm 29 | GEN_prf of term * thm 30 | GEN_ABS_prf of term option * term list * thm 31 | INST_TYPE_prf of (hol_type,hol_type)Lib.subst * thm 32 | INST_prf of (term,term)Lib.subst * thm 33 | MK_COMB_prf of thm * thm 34 | MP_prf of thm * thm 35 | NOT_INTRO_prf of thm 36 | NOT_ELIM_prf of thm 37 | REFL_prf of term 38 | SPEC_prf of term * thm 39 | SUBST_prf of (term,thm)Lib.subst * term * thm 40 | SYM_prf of thm 41 | TRANS_prf of thm * thm 42 | Beta_prf of thm 43 | Def_tyop_prf of {Thy:string,Tyop:string} * hol_type list * thm * hol_type 44 | Def_const_prf of {Thy:string,Name:string} * term 45 | Def_const_list_prf of string * (string * hol_type) list * thm 46 | Def_spec_prf of term list * thm 47 | Mk_abs_prf of thm * term * thm 48 | Mk_comb_prf of thm * thm * thm 49 | Specialize_prf of term * thm 50 | deductAntisym_prf of thm * thm 51 52 val proof : thm -> proof 53 val delete_proof : thm -> unit 54 val mk_proof_thm : proof -> term list * term -> thm 55 56 val deductAntisym : thm -> thm -> thm 57 58 val set_definition_callback : (thm -> unit) -> unit 59 val clear_definition_callback : unit -> unit 60 61end 62