src/HOL/Library/Countable_Set_Type.thy
changeset 69313 b021008c5397
parent 68406 6beb45f6cf67
child 69324 39ba40eb2150
     1.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -117,13 +117,13 @@
     1.4    is "UNION" parametric UNION_transfer by simp
     1.5  definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
     1.6  
     1.7 -lemma Union_conv_UNION: "\<Union>A = UNION A id"
     1.8 +lemma Union_conv_UNION: "\<Union>A = \<Union>(id ` A)"
     1.9  by auto
    1.10  
    1.11  lemma cUnion_transfer [transfer_rule]:
    1.12    "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
    1.13  proof -
    1.14 -  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
    1.15 +  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. \<Union>(id ` A)) (\<lambda>A. cUNION A id)"
    1.16      by transfer_prover
    1.17    then show ?thesis by (simp flip: cUnion_def)
    1.18  qed