| Wed, 28 Jan 2004 17:01:01 +0100 | paulson | tidying up arithmetic for the hyperreals | file | diff | annotate |
| Tue, 27 Jan 2004 15:39:51 +0100 | paulson | replacing HOL/Real/PRat, PNat by the rational number development | file | diff | annotate |
| Fri, 09 Jan 2004 10:46:18 +0100 | paulson | Defining the type class "ringpower" and deleting superseded theorems for | file | diff | annotate |
| Thu, 01 Jan 2004 10:06:32 +0100 | paulson | tweaking of lemmas in RealDef, RealOrd | file | diff | annotate |
| Mon, 24 Nov 2003 15:33:07 +0100 | paulson | conversion of integers to use Ring_and_Field; | file | diff | annotate |
| Mon, 30 Sep 2002 16:14:02 +0200 | berghofe | Adapted to new simplifier. | file | diff | annotate |
| Wed, 12 Dec 2001 19:21:02 +0100 | nipkow | mods due to reorienting and renaming of real_minus_mult_eq1/2 | file | diff | annotate |
| Fri, 16 Nov 2001 18:24:11 +0100 | paulson | even more theories from Jacques | file | diff | annotate |