1signature Defn =
2sig
3  include Abbrev
4
5  type thry   = TypeBasePure.typeBase
6  type proofs = Manager.proofs
7  type absyn  = Absyn.absyn
8  type pattern = Pmatch.pattern
9
10  val monitoring : bool ref
11
12  val ind_suffix : string ref
13  val def_suffix : string ref
14  val const_eq_ref : conv ref
15
16  val wfrec_eqns : thry -> term ->
17                    {SV : term list,
18                     WFR : term,
19                     extracta : (thm * term list * bool) list,
20                     pats : pattern list,
21                     proto_def : term}
22
23  val mk_defn    : string -> term -> defn
24  val mk_Rdefn   : string -> term -> term -> defn
25  val Hol_defn   : string -> term quotation -> defn
26  val Hol_Rdefn  : string -> term quotation -> term quotation -> defn
27  val mk_defns   : string list -> term list -> defn list
28  val Hol_defns  : string list -> term quotation -> defn list
29  val Hol_multi_defns : term quotation -> defn list
30
31  val name_of    : defn -> string
32  val eqns_of    : defn -> thm list
33  val ind_of     : defn -> thm option
34  val tcs_of     : defn -> term list
35  val reln_of    : defn -> term option
36  val params_of  : defn -> term list
37
38  val aux_defn   : defn -> defn option
39  val union_defn : defn -> defn option
40
41  val inst_defn  : defn -> (term,term)subst * (hol_type,hol_type)subst -> defn
42  val set_reln   : defn -> term -> defn
43
44  val elim_tcs   : defn -> thm list -> defn
45  val simp_tcs   : defn -> conv -> defn
46  val prove_tcs  : defn -> tactic -> defn
47
48  val triv_defn  : defn -> bool
49  val fetch_eqns : defn -> thm
50
51  val been_stored: string * thm -> unit
52  val store      : string * thm * thm -> unit
53  val save_defn  : defn -> unit
54
55  val parse_absyn : absyn -> term * string list
56  val parse_quote : term quotation -> term list
57
58  val tgoal      : defn -> proofs
59  val tprove0    : defn * tactic -> thm * thm
60  val tprove     : defn * tactic -> thm * thm
61  val tstore_defn : defn * tactic -> thm * thm
62
63  (* Do a termination proof without the DefnBase.defn object around.  The
64     first theorem should be the equations and the second the induction
65     principle, e.g., as written by Defn.save_defn. *)
66  val tgoal_no_defn  : (thm * thm) -> proofs
67  val tprove_no_defn : (thm * thm) * tactic -> thm * thm
68
69  val SUC_TO_NUMERAL_DEFN_CONV_hook : (term -> thm) ref
70
71end
72