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