diff -r 180f01d9df2c -r 213dcc39358f src/HOL/README.html
--- a/src/HOL/README.html	Mon May 12 19:54:43 2003 +0200
+++ b/src/HOL/README.html	Tue May 13 08:59:21 2003 +0200
@@ -28,15 +28,15 @@
 <dd>generic model of bytecode verification, i.e. data-flow analysis
 for assembly languages with subtypes
 
-<dt>HOL-Real
-<dd>a development of the reals and hyper-reals, which are used in
-non-standard analysis (builds the image HOL-Real)
+<dt>HOL-Complex
+<dd>a development of the complex numbers, the reals, and the hyper-reals,
+which are used in non-standard analysis (builds the image HOL-Complex)
 
-<dt>HOL-Real-HahnBanach
+<dt>HOL-Complex-HahnBanach
 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
 
-<dt>HOL-Real-ex
-<dd>miscellaneous real number examples
+<dt>HOL-Complex-ex
+<dd>miscellaneous real ans complex number examples
 
 <dt>Hoare
 <dd>verification of imperative programs (verification conditions are