--- a/src/HOL/Real/README.html Wed Apr 21 13:18:37 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<!-- $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>
\ No newline at end of file