hide newly introduced constants
authorhaftmann
Wed Sep 23 11:33:52 2009 +0200 (2009-09-23)
changeset 32647e54f47f9e28b
parent 32646 962b4354ed90
child 32649 442e03154ee6
child 32652 3175e23b79f3
child 32655 dd84779cd191
child 32700 e743ca6e97e7
hide newly introduced constants
src/HOL/Library/Executable_Set.thy
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Sep 22 11:26:46 2009 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 11:33:52 2009 +0200
     1.3 @@ -85,4 +85,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 +
     1.9  end
    1.10 \ No newline at end of file