1signature DefnBase =
2sig
3  type term = Term.term
4  type thm  = Thm.thm
5
6 datatype defn
7   = ABBREV  of {eqn:thm, bind:string}
8   | PRIMREC of {eqs:thm, ind:thm, bind:string}
9   | NONREC  of {eqs:thm, ind:thm, SV:term list, stem:string}
10   | STDREC  of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string}
11   | MUTREC  of {eqs:thm list, ind:thm, R:term,SV:term list,
12                 stem:string,union:defn}
13   | NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list,
14                 stem:string,aux:defn}
15   | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string}
16
17
18  val pp_defn : defn Parse.pprinter
19  val all_terms : defn -> term list
20    (* conclusions of theorems, SV variables, R *)
21
22  (* Used to control context tracking during termination
23     condition extraction *)
24
25  val read_congs  : unit -> thm list
26  val write_congs : thm list -> unit
27  val add_cong    : thm -> unit
28  val drop_cong   : term -> thm
29
30  val export_cong : string -> unit
31
32end
33