src/HOL/Number_Theory/Residues.thy
2014-01-30 haftmann 2014-01-30 more direct simplification rules for 1 div/mod numeral; added simplification rules for (- 1) div/mod numeral
2014-01-29 paulson 2014-01-29 minor adjustments
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-03-27 huffman 2012-03-27 remove redundant lemma
2011-09-10 wenzelm 2011-09-10 misc tuning;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-09-01 haftmann 2009-09-01 some reorganization of number theory