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