--- a/src/HOL/Real/HahnBanach/Bounds.thy Mon Dec 10 11:24:12 2007 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Mon Dec 10 11:24:14 2007 +0100
@@ -5,7 +5,9 @@
header {* Bounds *}
-theory Bounds imports Main Real begin
+theory Bounds
+imports Main Real
+begin
locale lub =
fixes A and x