explicitly hide empty, inter, union
authorhaftmann
Wed Sep 23 16:32:53 2009 +0200 (2009-09-23)
changeset 32702457135bdd596
parent 32701 5059a733a4b8
child 32703 7f9e05b3d0fb
explicitly hide empty, inter, union
src/HOL/Library/Executable_Set.thy
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Wed Sep 23 14:00:43 2009 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 16:32:53 2009 +0200
     1.3 @@ -100,6 +100,6 @@
     1.4    card                ("{*Fset.card*}")
     1.5    fold                ("{*foldl o flip*}")
     1.6  
     1.7 -hide (open) const subset eq_set Inter Union flip
     1.8 +hide (open) const empty inter union subset eq_set Inter Union flip
     1.9  
    1.10  end
    1.11 \ No newline at end of file