--- 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.