removed needless (and inconsistent) qualifier that messes up with Mirabelle
authorblanchet
Tue Mar 03 16:37:45 2015 +0100 (2015-03-03)
changeset 5957555f5e1cbf2a7
parent 59574 de392405a851
child 59576 913c4afb0388
removed needless (and inconsistent) qualifier that messes up with Mirabelle
src/HOL/Library/RBT_Impl.thy
     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 =