src/HOL/Library/Commutative_Ring.thy
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Mon, 10 Dec 2007 11:24:12 +0100 haftmann switched import from Main to List
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Fri, 20 Apr 2007 11:21:40 +0200 haftmann switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
Fri, 13 Apr 2007 21:26:35 +0200 wenzelm tuned document (headers, sections, spacing);
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Fri, 22 Sep 2006 13:04:30 +0200 wenzelm tuned proofs;
Tue, 19 Sep 2006 23:15:28 +0200 wenzelm tuned proofs;
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 20 Sep 2005 14:10:29 +0200 wenzelm added Commutative_Ring (from Main HOL);
less more (0) tip