src/HOL/Library/Fset.thy

 code_datatype Set Coset
 
 lemma member_code [code]:
   "member (Set xs) = List.member xs"
   "member (Coset xs) = Not \<circ> List.member xs"
-  by (simp_all add: ext_iff member_def fun_Compl_def bool_Compl_def)
+  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
 
 lemma member_image_UNIV [simp]:
   "member ` UNIV = UNIV"
 proof -
   have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"

   "inf A (Coset xs) = foldr remove xs A"
 proof -
   show "inf A (Set xs) = Set (List.filter (member A) xs)"
     by (simp add: inter project_def Set_def)
   have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
     fold More_Set.remove xs \<circ> member"
-    by (rule fold_apply) (simp add: ext_iff)
+    by (rule fold_apply) (simp add: fun_eq_iff)
   then have "fold More_Set.remove xs (member A) = 
     member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   then have "inf A (Coset xs) = fold remove xs A"
     by (simp add: Diff_eq [symmetric] minus_set *)
   moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
     by (auto simp add: More_Set.remove_def * intro: ext)
   ultimately show "inf A (Coset xs) = foldr remove xs A"

 lemma union_insert [code]:
   "sup (Set xs) A = foldr insert xs A"
   "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
 proof -
   have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
     fold Set.insert xs \<circ> member"
-    by (rule fold_apply) (simp add: ext_iff)
+    by (rule fold_apply) (simp add: fun_eq_iff)
   then have "fold Set.insert xs (member A) =
     member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   then have "sup (Set xs) A = fold insert xs A"
     by (simp add: union_set *)
   moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
     by (auto simp add: * intro: ext)
   ultimately show "sup (Set xs) A = foldr insert xs A"