Structure simpfrag


Source File Identifier index Theory binding index

signature simpfrag =
sig

  include Abbrev
  type convdata = { name: string,
                    key: (term list * term) option,
                    trace: int,
                    conv: (term list -> term -> thm) -> term list -> conv}

  type simpfrag = { convs: convdata list, rewrs: thm list}

  val empty_simpfrag : simpfrag
  val add_rwts : simpfrag -> thm list -> simpfrag

end;


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10