--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri May 07 20:34:05 2004 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sun May 09 16:39:29 2004 +0200
@@ -5,8 +5,6 @@
header {* Vector spaces *}
-(* theory VectorSpace = Aux: *)
-
theory VectorSpace = Real + Bounds + Zorn:
subsection {* Signature *}
--- a/src/HOL/Real/HahnBanach/document/root.tex Fri May 07 20:34:05 2004 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Sun May 09 16:39:29 2004 +0200
@@ -59,7 +59,6 @@
\part {Basic Notions}
\input{Bounds}
-\input{Aux}
\input{VectorSpace}
\input{Subspace}
\input{NormedSpace}