src/HOL/Hyperreal/README.html
author wenzelm
Tue, 20 Nov 2001 22:53:50 +0100
changeset 12254 78bc1f3462b5
parent 11544 97305ee424a9
child 14631 ec1e67f88f49
permissions -rw-r--r--
fixed links etc.;

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>

<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.

<UL>
<LI><A HREF="Zorn.html">Zorn</A>
Zorn's Lemma: proof based on the ZF version.

<LI><A HREF="Filter.html">Filter</A>
Theory of Filters and Ultrafilters.
Main result is a version of the Ultrafilter Theorem proved using
Zorn's Lemma. 

<LI><A HREF="HyperDef.html">HyperDef</A>
Ultrapower construction of the hyperreals

<LI><A HREF="NSA.html">NSA</A>
Theory defining sets of infinite numbers, infinitesimals, 
the infinitely close relation, and their various algebraic properties.

<LI><A HREF="HyperNat.html">HyperNat</A>
Ultrapower construction of the hypernaturals

<LI><A HREF="HyperPow.html">HyperPow</A>
Powers theory for the hyperreals

<LI><A HREF="Star.html">Star</A>
Nonstandard extensions of real sets and real functions

<LI><A HREF="NatStar.html">NatStar</A>
Nonstandard extensions of sets of naturals and functions on the natural
numbers

<LI><A HREF="SEQ.html">SEQ</A>
Theory of sequences developed using standard and nonstandard analysis

<LI><A HREF="Lim.html">Lim</A>
Theory of limits, continuous functions, and derivatives

<LI><A HREF="Series.html">Series</A>
Standard theory of finite summation and infinite series

</UL>

<P>Last modified on $Date$

<HR>

<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>