1.1 --- a/src/HOL/Library/Set_Algebras.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4    show "monoid_add.listsum set_plus {0::'a} = listsum_set"
     1.5      by (simp only: listsum_set_def)
     1.6    show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
     1.7 -    by (simp add: set_add.setsum_def setsum_set_def ext_iff)
     1.8 +    by (simp add: set_add.setsum_def setsum_set_def fun_eq_iff)
     1.9  qed
    1.10  
    1.11  interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.12 @@ -117,7 +117,7 @@
    1.13    show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
    1.14      by (simp add: power_set_def)
    1.15    show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
    1.16 -    by (simp add: set_mult.setprod_def setprod_set_def ext_iff)
    1.17 +    by (simp add: set_mult.setprod_def setprod_set_def fun_eq_iff)
    1.18  qed
    1.19  
    1.20  lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"