1.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri May 07 20:34:05 2004 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sun May 09 16:39:29 2004 +0200
1.3 @@ -5,8 +5,6 @@
1.4
1.5 header {* Vector spaces *}
1.6
1.7 -(* theory VectorSpace = Aux: *)
1.8 -
1.9 theory VectorSpace = Real + Bounds + Zorn:
1.10
1.11 subsection {* Signature *}
2.1 --- a/src/HOL/Real/HahnBanach/document/root.tex Fri May 07 20:34:05 2004 +0200
2.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex Sun May 09 16:39:29 2004 +0200
2.3 @@ -59,7 +59,6 @@
2.4 \part {Basic Notions}
2.5
2.6 \input{Bounds}
2.7 -\input{Aux}
2.8 \input{VectorSpace}
2.9 \input{Subspace}
2.10 \input{NormedSpace}