# 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