src/HOL/IntDiv.thy
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