1signature DataSize = 2sig 3 include Abbrev 4 5 val define_size : thm -> TypeBasePure.typeBase 6 -> {def : thm, 7 const_tyopl : (term * (string*string)) list} option 8 9end 10