| changeset 14710 | 247615bfffb8 |
| parent 14565 | c6dc17aab88a |
| child 14721 | 782932b1e931 |
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Thu May 06 20:43:30 2004 +0200 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri May 07 12:16:57 2004 +0200 @@ -5,7 +5,9 @@ header {* Vector spaces *} -theory VectorSpace = Aux: +(* theory VectorSpace = Aux: *) + +theory VectorSpace = Real + Bounds + Zorn: subsection {* Signature *}