equal
deleted
inserted
replaced
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
2 |
3 <HTML><HEAD><TITLE>HOL/Complex/README</TITLE> |
3 <!-- $Id$ --> |
4 <meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> |
4 |
5 </HEAD><BODY> |
5 <HTML> |
|
6 |
|
7 <HEAD> |
|
8 <meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> |
|
9 <TITLE>HOL/Complex/README</TITLE> |
|
10 </HEAD> |
|
11 |
|
12 <BODY> |
6 |
13 |
7 <H1>Complex: The Complex Numbers</H1> |
14 <H1>Complex: The Complex Numbers</H1> |
8 <P>This directory defines the type <KBD>complex</KBD> of the complex numbers, |
15 <P>This directory defines the type <KBD>complex</KBD> of the complex numbers, |
9 with numeric constants and some complex analysis. The development includes |
16 with numeric constants and some complex analysis. The development includes |
10 nonstandard analysis for the complex numbers. Note that the image |
17 nonstandard analysis for the complex numbers. Note that the image |
54 <li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions |
61 <li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions |
55 <li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions |
62 <li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions |
56 </ul> |
63 </ul> |
57 <HR> |
64 <HR> |
58 <P>Last modified $Date$ |
65 <P>Last modified $Date$ |
59 |
66 </BODY> |
60 </HTML> |
67 </HTML> |