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