src/HOL/Complex/README.html
changeset 14631 ec1e67f88f49
parent 14020 5fc9474833e5
child 14634 ffb4099c316f
--- 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>