<!-- $Id$ -->
<html>
<head>
<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
<title>HOL/Real/README</title>
</head>
<body>
<h2>Real: Dedekind Cut Construction of the Real Line</h2>
<ul>
<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
</ul>
<p>Last modified on $Date$</p>
<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>