equal
deleted
inserted
replaced
205 cterm_instantiate_pos cts rel_xtor_co_induct_thm |
205 cterm_instantiate_pos cts rel_xtor_co_induct_thm |
206 |> singleton (Proof_Context.export names_lthy lthy) |
206 |> singleton (Proof_Context.export names_lthy lthy) |
207 |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs) |
207 |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs) |
208 |> funpow n (fn thm => thm RS spec) |
208 |> funpow n (fn thm => thm RS spec) |
209 |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s) |
209 |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s) |
210 |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id |
210 |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id |
211 Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @ |
211 Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @ |
212 maps mk_fp_type_copy_thms fp_type_definitions @ |
212 maps mk_fp_type_copy_thms fp_type_definitions @ |
213 maps mk_type_copy_thms type_definitions) |
213 maps mk_type_copy_thms type_definitions) |
214 |> unfold_thms lthy @{thms subset_iff mem_Collect_eq |
214 |> unfold_thms lthy @{thms subset_iff mem_Collect_eq |
215 atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]} |
215 atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]} |