src/HOL/Divides.thy
2011-12-29 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-11-20 wenzelm eliminated obsolete "standard";
2011-11-16 huffman rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
2011-10-21 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-12 nipkow new fastforce replacing fastsimp - less confusing name
2011-09-07 huffman avoid using legacy theorem names
2011-06-29 wenzelm modernized some simproc setup;
2011-02-21 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-14 wenzelm eliminated global prems;
2010-09-17 nipkow added lemmas
2010-08-25 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-12 haftmann dropped superfluous [code del]s
2010-05-04 haftmann a ring_div is a ring_1_no_zero_divisors
2010-03-17 boehmes tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-09 haftmann weakend class ring_div; tuned
2010-03-08 haftmann transfer: avoid camel case
2010-02-24 haftmann lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
2010-02-18 huffman get rid of many duplicate simp rule warnings
2010-02-08 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-02 blanchet added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-02 nipkow removed legacy asm_lr
2009-12-18 blanchet polished Nitpick's binary integer support etc.;
2009-11-20 nipkow added lemma
2009-11-17 webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-17 webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-10-30 haftmann tuned code setup
2009-10-30 haftmann combined former theories Divides and IntDiv to one theory Divides
2009-10-29 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-28 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-10-28 haftmann moved lemmas for dvd on nat to theories Nat and Power
2009-07-15 wenzelm more antiquotations;
2009-07-14 haftmann code attributes use common underscore convention
2009-07-07 nipkow renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-16 huffman generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
2009-06-16 huffman move lemma div_power into semiring_div context; class ring_div inherits from idom
2009-04-28 haftmann dropped reference to class recpower and lemma duplicate
2009-04-16 haftmann tuned setups of CancelDivMod
2009-04-16 haftmann tightended specification of class semiring_div
2009-04-15 haftmann more coherent developement in Divides.thy and IntDiv.thy
2009-04-01 nipkow added nat_div_gt_0 [simp]
2009-04-01 nipkow added strong_setprod_cong[cong] (in analogy with setsum)
2009-03-26 wenzelm interpretation/interpret: prefixes are mandatory by default;
2009-03-22 haftmann lemma nat_dvd_not_less moved here from Arith_Tools
2009-03-12 haftmann merged
2009-03-12 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-12 nipkow added div lemmas
2009-03-04 blanchet Merge.
2009-03-04 blanchet Merge.
2009-03-03 nipkow removed and renamed redundant lemmas
2009-03-01 nipkow added lemmas by Jeremy Avigad
2009-02-24 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
2009-02-23 huffman move lemma dvd_mod_imp_dvd into class semiring_div
2009-02-22 nipkow added dvd_div_mult
2009-02-21 nipkow Removed subsumed lemmas
2009-02-20 nipkow removed subsumed lemmas
2009-02-18 huffman generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-02-17 nipkow Cleaned up IntDiv and removed subsumed lemmas.
2009-02-15 nipkow dvd and setprod lemmas
2009-01-28 nipkow Replaced group_ and ring_simps by algebra_simps;
less more (0) -100 -60 tip