--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/README.html	Wed Sep 29 15:35:09 1999 +0200
@@ -0,0 +1,27 @@
+<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
+
+<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
+
+Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
+
+This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
+following H. Heuser, Funktionalanalysis, p. 228 -232.
+The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
+It is a conclusion of Zorn's lemma.<P>
+
+Two different formaulations of the theorem are presented, one for general real vectorspaces
+and its application to normed vectorspaces. <P>
+
+The theorem says, that every continous linearform, defined on arbitrary subspaces
+(not only one-dimensional subspaces), can be extended to a continous linearform on
+the whole vectorspace.
+
+
+<HR>
+
+<ADDRESS>
+<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
+</ADDRESS>
+
+</BODY></HTML>
+