40 dtor_ctors = @{thms xtor_xtor}, |
40 dtor_ctors = @{thms xtor_xtor}, |
41 ctor_dtors = @{thms xtor_xtor}, |
41 ctor_dtors = @{thms xtor_xtor}, |
42 ctor_injects = @{thms xtor_inject}, |
42 ctor_injects = @{thms xtor_inject}, |
43 dtor_injects = @{thms xtor_inject}, |
43 dtor_injects = @{thms xtor_inject}, |
44 xtor_maps = [xtor_map], |
44 xtor_maps = [xtor_map], |
45 xtor_set_thmss = [xtor_sets], |
45 xtor_setss = [xtor_sets], |
46 xtor_rel_thms = [xtor_rel], |
46 xtor_rel_thms = [xtor_rel], |
47 xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}], |
47 xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}], |
48 xtor_co_rec_o_maps = [ctor_rec_o_map], |
48 xtor_co_rec_o_maps = [ctor_rec_o_map], |
49 xtor_rel_co_induct = xtor_rel_induct, |
49 xtor_rel_co_induct = xtor_rel_induct, |
50 dtor_set_inducts = [], |
50 dtor_set_inducts = [], |