--- a/src/HOL/Library/More_Set.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/More_Set.thy Mon Sep 13 11:13:15 2010 +0200
@@ -18,7 +18,7 @@
lemma fun_left_comm_idem_remove:
"fun_left_comm_idem remove"
proof -
- have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+ have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
show ?thesis by (simp only: fun_left_comm_idem_remove rem)
qed
@@ -26,7 +26,7 @@
assumes "finite A"
shows "B - A = Finite_Set.fold remove B A"
proof -
- have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+ have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
show ?thesis by (simp only: rem assms minus_fold_remove)
qed
@@ -124,6 +124,6 @@
lemma not_set_compl:
"Not \<circ> set xs = - set xs"
- by (simp add: fun_Compl_def bool_Compl_def comp_def ext_iff)
+ by (simp add: fun_Compl_def bool_Compl_def comp_def fun_eq_iff)
end