--- a/src/HOL/Library/Executable_Set.thy Wed Sep 23 08:26:12 2009 +0200 +++ b/src/HOL/Library/Executable_Set.thy Wed Sep 23 11:34:21 2009 +0200 @@ -100,4 +100,6 @@ card ("{*Fset.card*}") fold ("{*foldl o flip*}") +hide (open) const subset eq_set Inter Union flip + end \ No newline at end of file