src/HOL/Algebra/IntRing.thy
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;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 13 Nov 2009 22:01:01 +0100 nipkow moved lemma from Algebra/IntRing to Ring_and_Field
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Tue, 01 Sep 2009 16:00:57 +0200 haftmann some reorganization of number theory
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Sat, 10 Jan 2009 01:06:32 +0100 wenzelm fixed proof involving dvd;
Fri, 19 Dec 2008 11:09:09 +0100 ballarin More porting to new locales
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
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Tue, 02 Sep 2008 17:31:20 +0200 ballarin Interpretation commands no longer accept interpretation attributes.
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Wed, 30 Jul 2008 19:03:33 +0200 ballarin New locales for orders and lattices where the equivalence relation is not restricted to equality.
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Thu, 02 Aug 2007 18:13:42 +0200 ballarin Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
Tue, 24 Jul 2007 15:29:57 +0200 ballarin Interpretation of rings (as integers) maps defined operations to defined
Fri, 12 Jan 2007 15:37:21 +0100 ballarin Reverted to structure representation with records.
Fri, 22 Dec 2006 14:03:30 +0100 ballarin Experimenting with interpretations of "definition".
Mon, 16 Oct 2006 10:27:54 +0200 ballarin Order and lattice structures no longer based on records.
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
less more (0) tip