src/HOL/Complex/README.html
author kleing
Tue, 13 May 2003 08:59:21 +0200
changeset 14024 213dcc39358f
parent 14020 5fc9474833e5
child 14631 ec1e67f88f49
permissions -rw-r--r--
HOL-Real -> HOL-Complex

<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>