src/HOL/IntDiv.thy
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 nipkow 2009-03-01 removed redundant lemmas
2009-03-01 nipkow 2009-03-01 added lemmas by Jeremy Avigad
2009-02-23 huffman 2009-02-23 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
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-18 huffman 2009-02-18 generalize int_dvd_cancel_factor simproc to idom class
2009-02-17 huffman 2009-02-17 merged
2009-02-17 huffman 2009-02-17 remove redundant simp attributes for zdvd rules
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2009-02-16 haftmann 2009-02-16 added pdivmod on int (for code generation)
2009-01-31 nipkow 2009-01-31 added some simp rules
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-28 haftmann 2009-01-28 slightly adapted towards more uniformity with div/mod on nat
2009-01-08 huffman 2009-01-08 remove type-specific proofs
2009-01-08 huffman 2009-01-08 add class ring_div; generalize mod/diff/minus proofs for class ring_div
2009-01-08 huffman 2009-01-08 generalize zmod_zmod_cancel -> mod_mod_cancel
2009-01-08 huffman 2009-01-08 generalize some div/mod lemmas; remove type-specific proofs
2008-12-10 huffman 2008-12-10 move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-07-21 chaieb 2008-07-21 Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-04-02 haftmann 2008-04-02 moved some code lemmas for Numerals here
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-02-20 haftmann 2008-02-20 tuned structures in arith_data.ML
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-22 haftmann 2008-01-22 added class semiring_div
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-08-30 nipkow 2007-08-30 added lemma
2007-08-30 huffman 2007-08-30 ported div/mod simprocs from HOL/ex/Binary.thy
2007-08-21 huffman 2007-08-21 add lemma of_int_power
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-09 haftmann 2007-08-09 tuned
2007-07-25 nipkow 2007-07-25 Added lemmas
2007-07-24 nipkow 2007-07-24 Added cancel simprocs for dvd on nat and int
2007-07-19 haftmann 2007-07-19 added lemmas by Brian Huffman
2007-07-10 haftmann 2007-07-10 introduced (auxiliary) class dvd_mod for more convenient code generation
2007-06-28 haftmann 2007-06-28 code generation for dvd
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 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
2007-06-16 nipkow 2007-06-16 tuned
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 huffman 2007-06-11 modify proofs to avoid referring to int::nat=>int
2007-06-11 huffman 2007-06-11 add int_of_nat versions of lemmas about int::nat=>int
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;