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