--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/README.html Mon May 12 12:27:10 2003 +0200
@@ -0,0 +1,14 @@
+<HTML><HEAD><TITLE>HOL/Complex/README</TITLE></HEAD><BODY>
+
+<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>Complex</KBD> includes theories from the directories
+<KBD>HOL/Real</KBD> and <KBD>HOL/Hyperreal</KBD>.
+
+<HR>
+<P>Last modified $Date$
+
+</HTML>