| Sun, 15 Feb 2004 10:46:37 +0100 | paulson | Polymorphic treatment of binary arithmetic using axclasses | file | diff | annotate |
| Thu, 29 Jan 2004 16:51:17 +0100 | paulson | simplifications in the hyperreals | file | diff | annotate |
| Wed, 28 Jan 2004 17:01:01 +0100 | paulson | tidying up arithmetic for the hyperreals | file | diff | annotate |
| Mon, 12 Jan 2004 16:45:35 +0100 | paulson | Modified real arithmetic simplification | file | diff | annotate |
| Thu, 01 Jan 2004 10:06:32 +0100 | paulson | tweaking of lemmas in RealDef, RealOrd | file | diff | annotate |
| Sat, 27 Dec 2003 21:02:14 +0100 | paulson | re-organized numeric lemmas | file | diff | annotate |
| Mon, 22 Dec 2003 12:50:22 +0100 | paulson | moving HyperArith0.ML to other theories | file | diff | annotate |
| Fri, 19 Dec 2003 17:13:28 +0100 | paulson | tidying first part of HyperArith0.ML, using generic lemmas | file | diff | annotate |
| Sat, 30 Dec 2000 22:03:47 +0100 | paulson | separation of HOL-Hyperreal from HOL-Real | file | diff | annotate |