--- a/src/HOL/Complex/README.html Mon Apr 19 12:17:58 2004 +0200
+++ b/src/HOL/Complex/README.html Mon Apr 19 13:49:35 2004 +0200
@@ -1,14 +1,25 @@
-<HTML><HEAD><TITLE>HOL/Complex/README</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ </HEAD><BODY>
-<H1>Complex--The Complex Numbers</H1>
-
-<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
+<H1>Complex: The Complex Numbers</H1>
+ <P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
with numeric constants and some complex analysis. The development includes
nonstandard analysis for the complex numbers. Note that the image
<KBD>HOL-Complex</KBD> includes theories from the directories
-<KBD>HOL/Real</KBD> and <KBD>HOL/Hyperreal</KBD>.
+<KBD><a href="../Real/">HOL/Real</a></KBD> and <KBD><a href="../Hyperreal/">HOL/Hyperreal</a></KBD>.
+
-<HR>
+ <ul>
+ <li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
+ <li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
+ <li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
+ <li><a href="Complex.html">Complex</a> The complex numbers
+ <li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
+ <li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
+ <li><a href="NSInduct.html">NSInduct</a> Nonstandard induction for the hypernatural numbers
+ </ul>
+ <HR>
<P>Last modified $Date$
</HTML>