src/HOL/Library/RBT_Impl.thy
changeset 59575 55f5e1cbf2a7
parent 59554 4044f53326c9
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
     1.3 @@ -1195,7 +1195,7 @@
     1.4  done
     1.5  
     1.6  lemma rbtreeify_f_simps:
     1.7 -  "rbtreeify_f 0 kvs = (RBT_Impl.Empty, kvs)"
     1.8 +  "rbtreeify_f 0 kvs = (Empty, kvs)"
     1.9    "rbtreeify_f (Suc 0) ((k, v) # kvs) = 
    1.10    (Branch R Empty k v Empty, kvs)"
    1.11    "0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs =