src/HOL/Library/RBT_Impl.thy
changeset 39198 f967a16dfcdd
parent 37591 d3daea901123
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -1019,7 +1019,7 @@
     1.4  
     1.5  theorem lookup_map_entry:
     1.6    "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
     1.7 -  by (induct t) (auto split: option.splits simp add: expand_fun_eq)
     1.8 +  by (induct t) (auto split: option.splits simp add: ext_iff)
     1.9  
    1.10  
    1.11  subsection {* Mapping all entries *}
    1.12 @@ -1054,7 +1054,7 @@
    1.13  lemma fold_simps [simp, code]:
    1.14    "fold f Empty = id"
    1.15    "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
    1.16 -  by (simp_all add: fold_def expand_fun_eq)
    1.17 +  by (simp_all add: fold_def ext_iff)
    1.18  
    1.19  
    1.20  subsection {* Bulkloading a tree *}