| Mon, 16 Aug 2004 14:22:27 +0200 | nipkow | New theory header syntax. | file | diff | annotate |
| Thu, 29 Jul 2004 16:14:42 +0200 | paulson | removed some [iff] declarations from RealDef.thy, concerning inequalities | file | diff | annotate |
| Fri, 16 Jul 2004 17:31:44 +0200 | nipkow | Corrected TeX problems. | file | diff | annotate |
| Thu, 15 Jul 2004 15:32:32 +0200 | paulson | redefining sumr to be a translation to setsum | file | diff | annotate |
| Thu, 24 Jun 2004 17:52:02 +0200 | paulson | replaced monomorphic abs definitions by abs_if | file | diff | annotate |
| Thu, 26 Feb 2004 17:08:23 +0100 | paulson | converted Hyperreal/Series to Isar script | file | diff | annotate |
| Fri, 02 Nov 2001 17:55:24 +0100 | paulson | Numerals and simprocs for types real and hypreal. The abstract | file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 | wenzelm | sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, | file | diff | annotate |
| Sat, 30 Dec 2000 22:03:47 +0100 | paulson | separation of HOL-Hyperreal from HOL-Real | file | diff | annotate |