--- a/src/HOL/Library/RBT.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/RBT.thy Mon Sep 13 11:13:15 2010 +0200
@@ -112,7 +112,7 @@
lemma lookup_empty [simp]:
"lookup empty = Map.empty"
- by (simp add: empty_def lookup_RBT ext_iff)
+ by (simp add: empty_def lookup_RBT fun_eq_iff)
lemma lookup_insert [simp]:
"lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
@@ -144,7 +144,7 @@
lemma fold_fold:
"fold f t = More_List.fold (prod_case f) (entries t)"
- by (simp add: fold_def ext_iff RBT_Impl.fold_def entries_impl_of)
+ by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
lemma is_empty_empty [simp]:
"is_empty t \<longleftrightarrow> t = empty"
@@ -152,7 +152,7 @@
lemma RBT_lookup_empty [simp]: (*FIXME*)
"RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
- by (cases t) (auto simp add: ext_iff)
+ by (cases t) (auto simp add: fun_eq_iff)
lemma lookup_empty_empty [simp]:
"lookup t = Map.empty \<longleftrightarrow> t = empty"
@@ -220,7 +220,7 @@
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 ext_iff)
+ by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
lemma equal_Mapping [code]:
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"