# HG changeset patch
# User wenzelm
# Date 938717346 -7200
# Node ID 062a782d7402c52c91c7ce29601f2210d284bc60
# Parent  8c3190b173aa8408dbd17d7948b30c701a87db41
Real/HahnBanach;

diff -r 8c3190b173aa -r 062a782d7402 src/HOL/README.html
--- a/src/HOL/README.html	Thu Sep 30 16:16:56 1999 +0200
+++ b/src/HOL/README.html	Thu Sep 30 20:49:06 1999 +0200
@@ -47,7 +47,7 @@
 <DD>a simple theory of Input/Output Automata
 
 <DT>Isar_examples
-<DD>some Isabelle/Isar proof documents
+<DD>several Isabelle/Isar example proof documents
 
 <DT>Lambda
 <DD>a proof of the Church-Rosser theorem for lambda-calculus
@@ -63,6 +63,9 @@
 non-standard analysis.  Also includes the positive rationals.  Used to build
 the image HOL-Real.
 
+<DT>Real/HahnBanach
+<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+
 <DT>Subst
 <DD>defines a theory of substitution and unification.