src/HOL/Complex/README.html
author kleing
Fri, 26 Mar 2004 05:32:00 +0100
changeset 14486 74c053a25513
parent 14020 5fc9474833e5
child 14631 ec1e67f88f49
permissions -rw-r--r--
symbols in idents

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