# HG changeset patch
# User bauerg
# Date 1084113569 -7200
# Node ID 782932b1e931c2f6774f94131d6806a138254fef
# Parent  ceff6d4fb836f0f9d3114a9af3647c98b988b701
removed Aux.thy;

diff -r ceff6d4fb836 -r 782932b1e931 src/HOL/Real/HahnBanach/VectorSpace.thy
--- 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 *}
diff -r ceff6d4fb836 -r 782932b1e931 src/HOL/Real/HahnBanach/document/root.tex
--- 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}