# HG changeset patch
# User wenzelm
# Date 938186331 -7200
# Node ID 5f5d575ddac331a4c373cfcc719b4e2b62d42b63
# Parent  8a188ef6545e4e1065d02c57e48141ef979e2129
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
(in Isabelle/Isar) -- by Gertrud Bauer;

diff -r 8a188ef6545e -r 5f5d575ddac3 NEWS
--- a/NEWS	Fri Sep 24 16:33:57 1999 +0200
+++ b/NEWS	Fri Sep 24 17:18:51 1999 +0200
@@ -161,6 +161,9 @@
 
 ** HOL misc **
 
+* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
+(in Isabelle/Isar) -- by Gertrud Bauer;
+
 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
 -- avoids syntactic ambiguities and treats state, transition, and
 temporal levels more uniformly; introduces INCOMPATIBILITIES due to