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