# HG changeset patch
# User haftmann
# Date 1253698432 -7200
# Node ID e54f47f9e28b2d166da8609a0b714c7101441d3e
# Parent  962b4354ed90a6dd1545b2b7ab848519e4d4bc7c
hide newly introduced constants

diff -r 962b4354ed90 -r e54f47f9e28b src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Sep 22 11:26:46 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 11:33:52 2009 +0200
@@ -85,4 +85,6 @@
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
+hide (open) const subset eq_set Inter Union flip
+
 end
\ No newline at end of file