1signature newtypeTools =
2sig
3
4  include Abbrev
5  val rich_new_type : string * thm ->
6                      {absrep_id: thm,
7                       newty: hol_type,
8                       repabs_pseudo_id: thm,
9                       termP: term,
10                       termP_exists: thm,
11                       termP_term_REP: thm,
12                       term_ABS_t: term,
13                       term_ABS_pseudo11: thm,
14                       term_REP_t: term,
15                       term_REP_11: thm}
16
17end
18