equal
deleted
inserted
replaced
107 co_rec_discs = [], |
107 co_rec_discs = [], |
108 co_rec_disc_iffs = [], |
108 co_rec_disc_iffs = [], |
109 co_rec_selss = [], |
109 co_rec_selss = [], |
110 co_rec_codes = [], |
110 co_rec_codes = [], |
111 co_rec_transfers = [], |
111 co_rec_transfers = [], |
|
112 rec_o_maps = @{thms case_sum_o_map_sum}, |
112 common_rel_co_inducts = [], |
113 common_rel_co_inducts = [], |
113 rel_co_inducts = [], |
114 rel_co_inducts = [], |
114 common_set_inducts = [], |
115 common_set_inducts = [], |
115 set_inducts = []}} |
116 set_inducts = []}} |
116 end; |
117 end; |
172 co_rec_discs = [], |
173 co_rec_discs = [], |
173 co_rec_disc_iffs = [], |
174 co_rec_disc_iffs = [], |
174 co_rec_selss = [], |
175 co_rec_selss = [], |
175 co_rec_codes = [], |
176 co_rec_codes = [], |
176 co_rec_transfers = [], |
177 co_rec_transfers = [], |
|
178 rec_o_maps = @{thms case_prod_o_map_prod}, |
177 common_rel_co_inducts = [], |
179 common_rel_co_inducts = [], |
178 rel_co_inducts = [], |
180 rel_co_inducts = [], |
179 common_set_inducts = [], |
181 common_set_inducts = [], |
180 set_inducts = []}} |
182 set_inducts = []}} |
181 end; |
183 end; |