src/HOL/Divides.thy
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
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-12 nipkow 2009-03-12 added div lemmas
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 nipkow 2009-03-03 removed and renamed 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-23 huffman 2009-02-23 move lemma dvd_mod_imp_dvd into class semiring_div
2009-02-22 nipkow 2009-02-22 added dvd_div_mult
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-20 nipkow 2009-02-20 removed subsumed lemmas
2009-02-18 huffman 2009-02-18 generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2009-02-15 nipkow 2009-02-15 dvd and setprod lemmas
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
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-30 ballarin 2008-12-30 Merged.
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-11 nipkow 2008-12-11 codegen
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
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 haftmann 2008-07-21 (re-)added simp rules for (_ + _) div/mod _
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-11 haftmann 2008-07-11 separate class dvd for divisibility predicate