# HG changeset patch
# User wenzelm
# Date 1228947201 -3600
# Node ID 409d1ca929b5b931589cae2ba5c00c66348354f6
# Parent  d5a5888b8c54288d87e8c00f97eb030aca253a96
fixed import: requires ContNotDenum;

diff -r d5a5888b8c54 -r 409d1ca929b5 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Wed Dec 10 22:46:42 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Wed Dec 10 23:13:21 2008 +0100
@@ -6,7 +6,7 @@
 header {* Bounds *}
 
 theory Bounds
-imports Main Real
+imports Main ContNotDenum
 begin
 
 locale lub =