--- a/src/HOL/Library/Set_Algebras.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Tue Sep 07 10:05:19 2010 +0200
@@ -72,7 +72,7 @@
show "monoid_add.listsum set_plus {0::'a} = listsum_set"
by (simp only: listsum_set_def)
show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
- by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
+ by (simp add: set_add.setsum_def setsum_set_def ext_iff)
qed
interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
@@ -117,7 +117,7 @@
show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
by (simp add: power_set_def)
show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
- by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
+ by (simp add: set_mult.setprod_def setprod_set_def ext_iff)
qed
lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"