Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authorfleuriot
Thu, 21 Sep 2000 18:58:25 +0200
changeset 10055 2264bdd8becc
parent 10054 0afe7d951447
child 10056 9f84ffa4a8d0
*** empty log message ***
src/HOL/Real/Hyperreal/README.html file | annotate | diff | comparison | revisions 
--- a/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 18:47:18 2000 +0200
+++ b/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 18:58:25 2000 +0200
@@ -2,6 +2,9 @@
 <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
 
 <H2>Hyperreal--Ultrafilter 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>
 
 <UL>
 <LI><A HREF="Zorn.html">Zorn</A>
isabelle