# HG changeset patch
# User haftmann
# Date 1253716373 -7200
# Node ID 457135bdd59619146be3a9d9a0bc8a6abb1beaf7
# Parent  5059a733a4b8f2a0ff556c738f8119b95d484cf2
explicitly hide empty, inter, union

diff -r 5059a733a4b8 -r 457135bdd596 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Wed Sep 23 14:00:43 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 16:32:53 2009 +0200
@@ -100,6 +100,6 @@
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
-hide (open) const subset eq_set Inter Union flip
+hide (open) const empty inter union subset eq_set Inter Union flip
 
 end
\ No newline at end of file