equal
deleted
inserted
replaced
1195 end; |
1195 end; |
1196 |
1196 |
1197 val (ctor_rec_unique_thms, ctor_rec_unique_thm) = |
1197 val (ctor_rec_unique_thms, ctor_rec_unique_thm) = |
1198 `split_conj_thm (split_conj_prems n |
1198 `split_conj_thm (split_conj_prems n |
1199 (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |
1199 (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |
1200 |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @ |
1200 |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @ |
1201 map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); |
1201 map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); |
1202 |
1202 |
1203 val timer = time (timer "rec definitions & thms"); |
1203 val timer = time (timer "rec definitions & thms"); |
1204 |
1204 |
1205 val (ctor_induct_thm, induct_params) = |
1205 val (ctor_induct_thm, induct_params) = |