equal
deleted
inserted
replaced
39 val sum_prod_thms_set0 = |
39 val sum_prod_thms_set0 = |
40 @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff |
40 @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff |
41 Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp |
41 Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp |
42 mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps}; |
42 mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps}; |
43 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0; |
43 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0; |
44 val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply}; |
44 val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply}; |
45 |
45 |
46 fun hhf_concl_conv cv ctxt ct = |
46 fun hhf_concl_conv cv ctxt ct = |
47 (case Thm.term_of ct of |
47 (case Thm.term_of ct of |
48 Const (@{const_name all}, _) $ Abs _ => |
48 Const (@{const_name all}, _) $ Abs _ => |
49 Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct |
49 Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct |