diff -r 2e9314c07146 -r ec5c3d17969f src/HOL/Real/Hyperreal/README.html --- a/src/HOL/Real/Hyperreal/README.html Fri Nov 27 13:13:22 1998 +0100 +++ b/src/HOL/Real/Hyperreal/README.html Fri Nov 27 16:46:01 1998 +0100 @@ -5,7 +5,7 @@