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