# HG changeset patch
# User paulson
# Date 911833038 -3600
# Node ID 049305a4be67a51ae6c887a0e8e202f78578fd4c
# Parent a4600d21b59b62bb2b6763fada7026a15751fc54
fixed links
diff -r a4600d21b59b -r 049305a4be67 src/HOL/Real/README.html
--- a/src/HOL/Real/README.html Sat Nov 21 12:37:48 1998 +0100
+++ b/src/HOL/Real/README.html Mon Nov 23 15:57:18 1998 +0100
@@ -3,20 +3,17 @@
Real--Dedekind Cut Construction of the Real Line
-Requires Equiv.thy in the subdirectory HOL/Integ.
-
-- PNat The positive integers (very much the same as Nat.thy!)
-
- PRat The positive rationals
-
- PReal The positive reals constructed using Dedekind cuts
-
- Real The real numbers
-
- Lubs Definition of upper bounds, lubs and so on.
+
- PNat The positive integers (very much the same as Nat.thy!)
+
- PRat The positive rationals
+
- PReal The positive reals constructed using Dedekind cuts
+
- Real The real numbers
+
- Lubs Definition of upper bounds, lubs and so on.
(Useful e.g. in Fleuriot's NSA theory)
-
- RComplete Proof of completeness of reals in form of the supremum
+
- RComplete Proof of completeness of reals in form of the supremum
property. Also proofs that the reals have the Archimedean
property.
-
- RealAbs The absolute value function defined for the reals
+
- RealAbs The absolute value function defined for the reals
Last modified on $Date$