1signature NDDB = 2sig 3 4include Abbrev 5 6type rich_type = { 7 inj_pair : thm, 8 ret_map : thm, 9 all_tm : term, 10 all_thm : thm, 11 all_map : thm, 12 all_T : thm, 13 all_mono : thm 14} 15 16val types : (string list * rich_type list) ref 17 18val constantly_rich : rich_type 19 20val sum_all_def : thm 21val prod_all_def : thm 22val list_all_def : thm 23val option_all_def : thm 24val fun_all_def : thm 25 26val inj_pair_tm : term 27val J_tm : term 28 29val inj_constr_thm : thm 30val some_inj_thm : thm 31val k_inj_thm : thm 32 33val DEEP_SYM : thm -> thm 34 35end 36