Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed needless (and inconsistent) qualifier that messes up with Mirabelle
authorblanchet
Tue, 03 Mar 2015 16:37:45 +0100
changeset 59575 55f5e1cbf2a7
parent 59574 de392405a851
child 59576 913c4afb0388
removed needless (and inconsistent) qualifier that messes up with Mirabelle
src/HOL/Library/RBT_Impl.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Tue Mar 03 16:37:45 2015 +0100
@@ -1195,7 +1195,7 @@
 done
 
 lemma rbtreeify_f_simps:
-  "rbtreeify_f 0 kvs = (RBT_Impl.Empty, kvs)"
+  "rbtreeify_f 0 kvs = (Empty, kvs)"
   "rbtreeify_f (Suc 0) ((k, v) # kvs) = 
   (Branch R Empty k v Empty, kvs)"
   "0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs =
isabelle