src/HOL/Divides.thy
2012-03-27 huffman 2012-03-27 generalize more div/mod lemmas
2012-03-27 huffman 2012-03-27 generalize some theorems about div/mod
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 move int::ring_div instance upward, simplify several proofs
2012-03-27 huffman 2012-03-27 rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
2012-03-27 huffman 2012-03-27 extend definition of divmod_int_rel to handle denominator=0 case
2012-03-27 huffman 2012-03-27 tuned proofs
2012-03-27 huffman 2012-03-27 shorten a proof
2012-03-27 huffman 2012-03-27 simplify some proofs
2012-03-27 huffman 2012-03-27 rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
2012-03-27 huffman 2012-03-27 simplify some proofs
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-21 huffman 2012-02-21 remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
2012-02-20 bulwahn 2012-02-20 removing some unnecessary premises from Divides
2012-02-20 huffman 2012-02-20 simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-16 huffman 2011-11-16 rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
2011-10-21 bulwahn 2011-10-21 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 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-09-17 nipkow 2010-09-17 added lemmas
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-04 haftmann 2010-05-04 a ring_div is a ring_1_no_zero_divisors
2010-03-17 boehmes 2010-03-17 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-09 haftmann 2010-03-09 weakend class ring_div; tuned
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2010-02-24 haftmann 2010-02-24 lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-02 nipkow 2010-01-02 removed legacy asm_lr
2009-12-18 blanchet 2009-12-18 polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation
2009-11-20 nipkow 2009-11-20 added lemma
2009-11-17 webertj 2009-11-17 Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-17 webertj 2009-11-17 Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-30 haftmann 2009-10-30 combined former theories Divides and IntDiv to one theory Divides
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-10-28 haftmann 2009-10-28 moved lemmas for dvd on nat to theories Nat and Power
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-15 huffman 2009-06-15 generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
2009-06-15 huffman 2009-06-15 move lemma div_power into semiring_div context; class ring_div inherits from idom
2009-04-28 haftmann 2009-04-28 dropped reference to class recpower and lemma duplicate
2009-04-16 haftmann 2009-04-16 tuned setups of CancelDivMod
2009-04-16 haftmann 2009-04-16 tightended specification of class semiring_div
2009-04-15 haftmann 2009-04-15 more coherent developement in Divides.thy and IntDiv.thy
2009-04-01 nipkow 2009-04-01 added nat_div_gt_0 [simp]
2009-04-01 nipkow 2009-04-01 added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-22 haftmann 2009-03-22 lemma nat_dvd_not_less moved here from Arith_Tools
2009-03-12 haftmann 2009-03-12 merged