| Wed, 19 Nov 2003 14:29:06 +0100 | paulson | additions to Ring_and_Field | file | diff | annotate |
| Tue, 18 Nov 2003 11:03:33 +0100 | paulson | new theorems for Rings | file | diff | annotate |
| Thu, 08 Aug 2002 23:48:31 +0200 | wenzelm | proper instantiation of mk_left_commute; | file | diff | annotate |
| Wed, 07 Aug 2002 20:05:43 +0200 | wenzelm | mk_left_commute: proper instantiation avoids expensive unification; | file | diff | annotate |
| Wed, 31 Jul 2002 16:10:24 +0200 | nipkow | added mk_left_commute to HOL.thy and used it "everywhere" | file | diff | annotate |
| Tue, 23 Oct 2001 22:58:15 +0200 | wenzelm | eliminated old numerals; | file | diff | annotate |
| Mon, 15 Oct 2001 20:34:44 +0200 | wenzelm | GPLed; | 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 |
| Mon, 12 Feb 2001 20:43:12 +0100 | wenzelm | \<subseteq>; | file | diff | annotate |
| Sat, 20 Jan 2001 00:34:46 +0100 | wenzelm | instance int :: ordered_ring moved to Ring_and_Field_Example, because | file | diff | annotate |
| Wed, 06 Dec 2000 22:10:11 +0100 | wenzelm | unsymbolize; | file | diff | annotate |
| Wed, 06 Dec 2000 21:53:05 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 06 Dec 2000 17:03:26 +0100 | bauerg | some derived properties; | file | diff | annotate |
| Thu, 30 Nov 2000 14:10:23 +0100 | bauerg | some properties; | file | diff | annotate |
| Tue, 21 Nov 2000 16:25:32 +0100 | bauerg | ; | file | diff | annotate |
| Sat, 18 Nov 2000 19:47:12 +0100 | wenzelm | axclass ordered_ring; | file | diff | annotate |
| Sat, 18 Nov 2000 00:32:08 +0100 | wenzelm | added axclass ordered_field; | file | diff | annotate |
| Fri, 17 Nov 2000 18:49:09 +0100 | wenzelm | tuned; | file | diff | annotate |
| Thu, 16 Nov 2000 23:12:58 +0100 | bauerg | rings and fields; | file | diff | annotate |