Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.
<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>HOL-Complex</KBD> includes theories from the directories
<KBD>HOL/Real</KBD> and <KBD>HOL/Hyperreal</KBD>.
<HR>
<P>Last modified $Date$
</HTML>