# HG changeset patch
# User nipkow
# Date 1181149960 -7200
# Node ID 4e61c67a87e38270ae89128d98b4787f51653841
# Parent  e39dd93161d90fc92cdcbf5860b22f52f9020683
hide filter

diff -r e39dd93161d9 -r 4e61c67a87e3 src/HOL/Hyperreal/Filter.thy
--- a/src/HOL/Hyperreal/Filter.thy	Wed Jun 06 19:12:07 2007 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Wed Jun 06 19:12:40 2007 +0200
@@ -402,4 +402,6 @@
 
 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex
 
+hide (open) const filter
+
 end