1signature ind_types = 2sig 3 include Abbrev 4 type constructor = string * hol_type list 5 type tyspec = hol_type * constructor list 6 7 val define_type : tyspec list -> {induction:thm, recursion:thm} 8 9end 10