# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1464849263 -7200
# Node ID a5697f7a33223c860c18538d9c01da45b349fe2f
# Parent  2cddda300fc787fb47fe1b37a3b7431baddab5e2
Hid RBT.filter

diff -r 2cddda300fc7 -r a5697f7a3322 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Wed Jun 01 22:35:51 2016 +0200
+++ b/src/HOL/Library/RBT.thy	Thu Jun 02 08:34:23 2016 +0200
@@ -233,8 +233,8 @@
 lifting_forget rbt.lifting
 
 hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi 
-  is_empty
+  is_empty filter
 hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def 
-  union_def insert_def map_entry_def foldi_def is_empty_def
+  union_def insert_def map_entry_def foldi_def is_empty_def filter_def
 
 end