src/HOL/IntDiv.thy
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 01 Mar 2009 12:01:57 +0100 nipkow removed redundant lemmas
Sun, 01 Mar 2009 10:24:57 +0100 nipkow added lemmas by Jeremy Avigad
Mon, 23 Feb 2009 16:25:52 -0800 huffman make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Sat, 21 Feb 2009 09:58:26 +0100 nipkow removed redundant thms
Fri, 20 Feb 2009 23:46:03 +0100 nipkow Removed redundant lemmas
Wed, 18 Feb 2009 15:01:53 -0800 huffman generalize int_dvd_cancel_factor simproc to idom class
Tue, 17 Feb 2009 10:52:55 -0800 huffman merged
Tue, 17 Feb 2009 07:13:29 -0800 huffman remove redundant simp attributes for zdvd rules
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Mon, 16 Feb 2009 19:11:15 +0100 haftmann added pdivmod on int (for code generation)
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 28 Jan 2009 11:02:11 +0100 haftmann slightly adapted towards more uniformity with div/mod on nat
Thu, 08 Jan 2009 12:25:22 -0800 huffman remove type-specific proofs
Thu, 08 Jan 2009 09:12:29 -0800 huffman add class ring_div; generalize mod/diff/minus proofs for class ring_div
Thu, 08 Jan 2009 08:36:16 -0800 huffman generalize zmod_zmod_cancel -> mod_mod_cancel
Thu, 08 Jan 2009 08:24:08 -0800 huffman generalize some div/mod lemmas; remove type-specific proofs
Wed, 10 Dec 2008 07:52:54 -0800 huffman move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Mon, 21 Jul 2008 13:36:44 +0200 chaieb Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Wed, 02 Apr 2008 15:58:26 +0200 haftmann moved some code lemmas for Numerals here
Sat, 29 Mar 2008 19:14:00 +0100 wenzelm replaced 'ML_setup' by 'ML';
Wed, 20 Feb 2008 14:52:38 +0100 haftmann tuned structures in arith_data.ML
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Fri, 25 Jan 2008 14:53:52 +0100 haftmann moved definition of power on ints to theory Int
Tue, 22 Jan 2008 23:07:21 +0100 haftmann added class semiring_div
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Fri, 07 Dec 2007 15:07:59 +0100 haftmann instantiation target rather than legacy instance
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:33 +0200 chaieb fixed proofs
Fri, 12 Oct 2007 08:20:46 +0200 haftmann class div inherits from class times
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Thu, 30 Aug 2007 21:43:08 +0200 nipkow added lemma
Thu, 30 Aug 2007 05:01:38 +0200 huffman ported div/mod simprocs from HOL/ex/Binary.thy
Tue, 21 Aug 2007 20:51:10 +0200 huffman add lemma of_int_power
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Thu, 09 Aug 2007 15:52:45 +0200 haftmann tuned
Wed, 25 Jul 2007 18:10:28 +0200 nipkow Added lemmas
Tue, 24 Jul 2007 19:58:53 +0200 nipkow Added cancel simprocs for dvd on nat and int
Thu, 19 Jul 2007 21:47:38 +0200 haftmann added lemmas by Brian Huffman
Tue, 10 Jul 2007 09:23:10 +0200 haftmann introduced (auxiliary) class dvd_mod for more convenient code generation
Thu, 28 Jun 2007 19:09:34 +0200 haftmann code generation for dvd
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Wed, 20 Jun 2007 05:18:39 +0200 huffman change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
Sat, 16 Jun 2007 16:27:35 +0200 nipkow tuned
Wed, 13 Jun 2007 03:31:11 +0200 huffman removed constant int :: nat => int;
Mon, 11 Jun 2007 05:20:05 +0200 huffman modify proofs to avoid referring to int::nat=>int
Mon, 11 Jun 2007 02:25:55 +0200 huffman add int_of_nat versions of lemmas about int::nat=>int
Thu, 31 May 2007 18:16:52 +0200 wenzelm moved Integ files to canonical place;
less more (0) tip