src/HOL/Library/RBT.thy

   "RBT_Impl.keys (impl_of t) = keys t"
   by (simp add: keys_def)
 
 lemma lookup_empty [simp]:
   "lookup empty = Map.empty"
-  by (simp add: empty_def lookup_RBT expand_fun_eq)
+  by (simp add: empty_def lookup_RBT ext_iff)
 
 lemma lookup_insert [simp]:
   "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
   by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
 

   "lookup (map f t) k = Option.map (f k) (lookup t k)"
   by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
 
 lemma fold_fold:
   "fold f t = More_List.fold (prod_case f) (entries t)"
-  by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of)
+  by (simp add: fold_def ext_iff RBT_Impl.fold_def entries_impl_of)
 
 lemma is_empty_empty [simp]:
   "is_empty t \<longleftrightarrow> t = empty"
   by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
 
 lemma RBT_lookup_empty [simp]: (*FIXME*)
   "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
-  by (cases t) (auto simp add: expand_fun_eq)
+  by (cases t) (auto simp add: ext_iff)
 
 lemma lookup_empty_empty [simp]:
   "lookup t = Map.empty \<longleftrightarrow> t = empty"
   by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
 

   "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
   by (rule mapping_eqI) (simp add: map_of_map_restrict)
 
 lemma bulkload_Mapping [code]:
   "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
-  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
+  by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
 
 lemma equal_Mapping [code]:
   "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
   by (simp add: equal Mapping_def entries_lookup)