# HG changeset patch
# User haftmann
# Date 1253698461 -7200
# Node ID e743ca6e97e7fed00ad98f674bedd2f7bf57636d
# Parent  e54f47f9e28b2d166da8609a0b714c7101441d3e# Parent  250b4d8342ca2d561c32405a44a282c58e8d52b1
merged

diff -r 250b4d8342ca -r e743ca6e97e7 src/HOL/Library/Executable_Set.thy
--- 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