src/HOL/Algebra/Ring.thy
Wed, 05 Mar 2014 21:51:30 +0100 wenzelm more symbols;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 23 Apr 2012 21:44:36 +0200 wenzelm more standard method setup;
Mon, 09 Apr 2012 21:29:47 +0200 wenzelm tuned proofs;
Mon, 27 Feb 2012 21:07:00 +0100 wenzelm tuned proofs;
Sat, 03 Sep 2011 22:05:25 +0200 wenzelm misc tuning and simplification of proofs;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Thu, 06 Jan 2011 21:06:17 +0100 ballarin Abelian group facts obtained from group facts via interpretation (sublocale).
Sun, 21 Mar 2010 17:12:31 +0100 wenzelm standard headers;
Sun, 21 Mar 2010 16:51:37 +0100 wenzelm slightly more uniform definitions -- eliminated old-style meta-equality;
Sun, 21 Mar 2010 15:57:40 +0100 wenzelm eliminated old constdefs;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Tue, 16 Dec 2008 21:10:53 +0100 ballarin More porting to new locales.
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Mon, 18 Aug 2008 17:57:06 +0200 ballarin Theorem on polynomial division and lemmas.
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Thu, 31 Jul 2008 09:49:21 +0200 ballarin Tuned (for the sake of a meaningless log entry).
Tue, 29 Jul 2008 16:17:45 +0200 ballarin New theorems on summation.
Tue, 15 Jul 2008 16:50:09 +0200 ballarin Removed uses of context element includes.
Wed, 05 Mar 2008 21:33:59 +0100 wenzelm explicit referencing of background facts;
Tue, 24 Jul 2007 15:29:57 +0200 ballarin Interpretation of rings (as integers) maps defined operations to defined
Wed, 13 Jun 2007 00:01:41 +0200 wenzelm tuned proofs: avoid implicit prems;
Wed, 07 Feb 2007 17:32:52 +0100 berghofe Adapted to changes in Finite_Set theory.
Fri, 22 Dec 2006 14:03:30 +0100 ballarin Experimenting with interpretations of "definition".
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
less more (0) tip