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