# HG changeset patch
# User fleuriot
# Date 969555505 -7200
# Node ID 2264bdd8becc497f706b21c39d0789f5d4cfc52a
# Parent 0afe7d9514475bcf666c3b68495c6ce2ce7a1e53
*** empty log message ***
diff -r 0afe7d951447 -r 2264bdd8becc src/HOL/Real/Hyperreal/README.html
--- 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 @@
HOL/Real/README
Hyperreal--Ultrafilter Construction of the Non-Standard Reals
+ See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
+Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
+