equal
deleted
inserted
replaced
40 val sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
40 val sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
41 val sum_prod_thms_set = |
41 val sum_prod_thms_set = |
42 @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff |
42 @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff |
43 Union_Un_distrib image_iff o_apply map_prod_simp |
43 Union_Un_distrib image_iff o_apply map_prod_simp |
44 mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
44 mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
45 val sum_prod_thms_rel = @{thms prod_rel_apply rel_sum_simps id_apply}; |
45 val sum_prod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply}; |
46 |
46 |
47 fun hhf_concl_conv cv ctxt ct = |
47 fun hhf_concl_conv cv ctxt ct = |
48 (case Thm.term_of ct of |
48 (case Thm.term_of ct of |
49 Const (@{const_name all}, _) $ Abs _ => |
49 Const (@{const_name all}, _) $ Abs _ => |
50 Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct |
50 Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct |