--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/README.html Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,38 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Hahn_Banach/README</TITLE>
+</HEAD>
+
+<BODY>
+
+<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
+
+Author: Gertrud Bauer, Technische Universität Mü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>