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