Structure DataSize

Source File	Identifier index	Theory binding index

signature DataSize =
sig
  include Abbrev

  val prove_size_eqs : bool ref

  val define_size : {induction:thm, recursion:thm}
                        -> TypeBasePure.typeBase
                        -> {def : thm,
                            const_tyopl : (term * (string*string)) list} option

end

Source File	Identifier index	Theory binding index

HOL 4, Trindemossen-1