# HG changeset patch
# User fleuriot
# Date 970747496 -7200
# Node ID 9d4d5852eb478708f28fbb27444d9a52f95be8ce
# Parent  6263a4a60e38ddf8460a0d6b5dbe3a8527c45f7e
Updated README file for HOL/Real

diff -r 6263a4a60e38 -r 9d4d5852eb47 src/HOL/Real/Hyperreal/Star.ML
--- a/src/HOL/Real/Hyperreal/Star.ML	Wed Oct 04 22:21:10 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Star.ML	Thu Oct 05 14:04:56 2000 +0200
@@ -492,6 +492,12 @@
 by (Fuf_tac 1);
 qed "inf_close_FreeUltrafilterNat_iff";
 
+Goal "inj starfun";
+by (rtac injI 1);
+by (rtac ext 1 THEN rtac ccontr 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1);
+by (auto_tac (claset(),simpset() addsimps [starfun]));
+qed "inj_starfun";
 
 
 
diff -r 6263a4a60e38 -r 9d4d5852eb47 src/HOL/Real/README.html
--- a/src/HOL/Real/README.html	Wed Oct 04 22:21:10 2000 +0200
+++ b/src/HOL/Real/README.html	Thu Oct 05 14:04:56 2000 +0200
@@ -7,13 +7,71 @@
 <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="Real.html">Real</A>  The real numbers
+<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$