Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/RBT.thy
changeset 46133 d9fe85d3d2cd
parent 45928 874845660119
child 46565 ad21900e0ee9 
--- a/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -146,7 +146,7 @@
   by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
 
 lemma fold_fold:
-  "fold f t = More_List.fold (prod_case f) (entries t)"
+  "fold f t = List.fold (prod_case f) (entries t)"
   by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
 
 lemma is_empty_empty [simp]:
isabelle