Structure DataSize


Source File Identifier index Theory binding index

signature DataSize =
sig
  include Abbrev

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

end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10