Structure DefnBase

signature DefnBase =
sig
  include DefnBaseCore
  datatype defn
   = ABBREV  of {eqn:thm, bind:string}
   | PRIMREC of {eqs:thm, ind:thm, bind:string}
   | NONREC  of {eqs:thm, ind:thm, SV:term list, stem:string}
   | STDREC  of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string}
   | MUTREC  of {eqs:thm list, ind:thm, R:term,SV:term list,
                 stem:string,union:defn}
   | NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list,
                 stem:string,aux:defn}
   | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string}


  val pp_defn : defn Parse.pprinter
  val all_terms : defn -> term list
    (* conclusions of theorems, SV variables, R *)

  (* Used to control context tracking during termination
     condition extraction *)

  val read_congs  : unit -> thm list
  val write_congs : thm list -> unit
  val add_cong    : thm -> unit
  val drop_cong   : term -> thm

  val export_cong : string -> unit

  (* record various flavours of definition, keyed by constant and a
     "tag", which is a user-choosable string. Assume that "user" and
     "compute" exist for example.

     Another might be "PMATCH", which would be the definition with
     case constants translated into PMATCH versions.

     For the moment, as per all the names that talk of "userdefs", the
     only useful tag is "user".
  *)

  val const_eq_ref : Abbrev.conv ref
  val elim_triv_literal_CONV : Abbrev.conv
  val one_line_ify : PmatchHeuristics.pmatch_heuristic option -> thm -> thm
  val LIST_HALF_MK_ABS : thm -> thm

end

HOL 4, Trindemossen-1