1.1 --- a/NEWS	Fri Sep 24 16:33:57 1999 +0200
     1.2 +++ b/NEWS	Fri Sep 24 17:18:51 1999 +0200
     1.3 @@ -161,6 +161,9 @@
     1.4  
     1.5  ** HOL misc **
     1.6  
     1.7 +* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
     1.8 +(in Isabelle/Isar) -- by Gertrud Bauer;
     1.9 +
    1.10  * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
    1.11  -- avoids syntactic ambiguities and treats state, transition, and
    1.12  temporal levels more uniformly; introduces INCOMPATIBILITIES due to