src/HOL/Lifting_Set.thy
changeset 56166 9a241bc276cd
parent 55945 e96383acecf9
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Lifting_Set.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Set.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  
     1.5  lemma UNION_transfer [transfer_rule]:
     1.6    "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
     1.7 -  unfolding SUP_def [abs_def] by transfer_prover
     1.8 +  unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
     1.9  
    1.10  lemma Ball_transfer [transfer_rule]:
    1.11    "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"