| Wed, 14 Jan 2004 00:13:04 +0100 | nipkow | Told linear arithmetic package about injections "real" from nat/int into real. | 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 |
| Tue, 23 Dec 2003 18:24:16 +0100 | paulson | removing real_of_posnat | file | diff | annotate |
| Tue, 23 Dec 2003 17:41:52 +0100 | paulson | converting Hyperreal/NthRoot to Isar | file | diff | annotate |
| Thu, 27 Nov 2003 10:47:55 +0100 | paulson | Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. | file | diff | annotate |
| Thu, 15 Nov 2001 16:12:49 +0100 | paulson | new theories from Jacques Fleuriot | file | diff | annotate |