changeset 36176 | 3fe7e97ccca8 |
parent 36147 | b43b22f63665 |
child 37458 | 4a76497f2eaa |
--- a/src/HOL/Library/RBT_Impl.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Fri Apr 16 21:28:09 2010 +0200 @@ -1079,6 +1079,6 @@ then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def) qed -hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted +hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted end