<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
<H2>Real--Dedekind Cut Construction of the Real Line</H2>
<UL>
<LI><A HREF="PNat.html">PNat</A> The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!)
<LI><A HREF="PRat.html">PRat</A> The positive rationals
<LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts
<LI><A HREF="RealDef.html">RealDef</A> The real numbers
<LI><A HREF="RealOrd.html">RealOrd</A> More real numbers theorems- ordering
properties
<LI><A HREF="RealInt.html">RealInt</A> Embedding of the integers in the reals
<LI><A HREF="RealBin.html">RealBin</A> Binary arithmetic for the reals
<LI><A HREF="Lubs.html">Lubs</A> Definition of upper bounds, lubs and so on.
(Useful e.g. in Fleuriot's NSA theory)
<LI><A HREF="RComplete.html">RComplete</A> Proof of completeness of reals in form of the supremum
property. Also proofs that the reals have the Archimedean
property.
<LI><A HREF="RealAbs.html">RealAbs</A> The absolute value function defined for the reals
</ul>
<H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2>
<LI> 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 <A HREF="../../../ZF/Zorn.html">ZF version</A>
<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="HyperOrd.html">HyperOrd</A>
More hyperreal numbers theorems- ordering properties
<LI><A HREF="HRealAbs.html">HRealAbs</A> The absolute value function
defined for 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>