--- a/src/HOL/HahnBanach/README.html Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-<!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/Real/HahnBanach/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>