src/HOL/Algebra/Exponent.thy
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Tue, 10 Jun 2008 15:30:54 +0200 haftmann slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Thu, 27 Sep 2007 17:55:28 +0200 paulson removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
Tue, 24 Jul 2007 23:55:28 +0200 wenzelm fixed proofs involving dvd;
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
Wed, 02 Aug 2006 16:50:41 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Fri, 01 Jul 2005 17:41:10 +0200 nipkow prime is a predicate now.
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 09 Jun 2004 11:18:51 +0200 paulson moved some cardinality results into main HOL
Thu, 06 May 2004 14:14:18 +0200 wenzelm tuned document;
Tue, 18 Mar 2003 18:07:06 +0100 paulson moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
less more (0) tip