*** empty log message ***
authorfleuriot
Thu Sep 21 18:58:25 2000 +0200 (2000-09-21)
changeset 100552264bdd8becc
parent 10054 0afe7d951447
child 10056 9f84ffa4a8d0
*** empty log message ***
src/HOL/Real/Hyperreal/README.html
     1.1 --- a/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 18:47:18 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 18:58:25 2000 +0200
     1.3 @@ -2,6 +2,9 @@
     1.4  <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
     1.5  
     1.6  <H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
     1.7 +<LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
     1.8 +Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
     1.9 +<UL>
    1.10  
    1.11  <UL>
    1.12  <LI><A HREF="Zorn.html">Zorn</A>