src/HOL/README.html
changeset 14024 213dcc39358f
parent 13852 dd2cd94a51e6
child 14543 0e266a5dd6e3
     1.1 --- a/src/HOL/README.html	Mon May 12 19:54:43 2003 +0200
     1.2 +++ b/src/HOL/README.html	Tue May 13 08:59:21 2003 +0200
     1.3 @@ -28,15 +28,15 @@
     1.4  <dd>generic model of bytecode verification, i.e. data-flow analysis
     1.5  for assembly languages with subtypes
     1.6  
     1.7 -<dt>HOL-Real
     1.8 -<dd>a development of the reals and hyper-reals, which are used in
     1.9 -non-standard analysis (builds the image HOL-Real)
    1.10 +<dt>HOL-Complex
    1.11 +<dd>a development of the complex numbers, the reals, and the hyper-reals,
    1.12 +which are used in non-standard analysis (builds the image HOL-Complex)
    1.13  
    1.14 -<dt>HOL-Real-HahnBanach
    1.15 +<dt>HOL-Complex-HahnBanach
    1.16  <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    1.17  
    1.18 -<dt>HOL-Real-ex
    1.19 -<dd>miscellaneous real number examples
    1.20 +<dt>HOL-Complex-ex
    1.21 +<dd>miscellaneous real ans complex number examples
    1.22  
    1.23  <dt>Hoare
    1.24  <dd>verification of imperative programs (verification conditions are