equal
deleted
inserted
replaced
1 <!-- $Id$ --> |
1 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY> |
2 <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY> |
3 |
3 |
4 <H2>Real--Dedekind Cut Construction of the Real Line</H2> |
4 <H2>Real--Dedekind Cut Construction of the Real Line</H2> |
5 |
5 |
6 <UL> |
6 <ul> |
7 <LI><A HREF="PNat.html">PNat</A> The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!) |
7 <LI><A HREF="PNat.html">PNat</A> The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!) |
8 <LI><A HREF="PRat.html">PRat</A> The positive rationals |
8 <LI><A HREF="PRat.html">PRat</A> The positive rationals |
9 <LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts |
9 <LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts |
10 <LI><A HREF="RealDef.html">RealDef</A> The real numbers |
10 <LI><A HREF="RealDef.html">RealDef</A> The real numbers |
11 <LI><A HREF="RealOrd.html">RealOrd</A> More real numbers theorems- ordering |
11 <LI><A HREF="RealOrd.html">RealOrd</A> More real numbers theorems- ordering |
20 property. |
20 property. |
21 <LI><A HREF="RealAbs.html">RealAbs</A> The absolute value function defined for the reals |
21 <LI><A HREF="RealAbs.html">RealAbs</A> The absolute value function defined for the reals |
22 </ul> |
22 </ul> |
23 |
23 |
24 <H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2> |
24 <H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2> |
25 <LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard |
25 |
26 Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. |
26 <p> |
|
27 See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real |
|
28 Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. |
|
29 </p> |
27 |
30 |
28 <UL> |
31 <UL> |
29 <LI><A HREF="Zorn.html">Zorn</A> |
32 <LI><A HREF="Zorn.html">Zorn</A> |
30 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A> |
33 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A> |
31 |
34 |