src/HOL/Divides.thy
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
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-02-20 haftmann 2008-02-20 using only an relation predicate to construct div and mod
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-02-13 haftmann 2008-02-13 more abstract lemmas
2008-01-23 wenzelm 2008-01-23 tuned proofs;
2008-01-22 haftmann 2008-01-22 added class semiring_div
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-10-23 nipkow 2007-10-23 went back to >0
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-16 haftmann 2007-10-16 global class syntax
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-14 huffman 2007-08-14 minimize imports
2007-07-24 haftmann 2007-07-24 using class target
2007-07-10 haftmann 2007-07-10 introduced (auxiliary) class dvd_mod for more convenient code generation
2007-05-31 wenzelm 2007-05-31 removed dead code;
2007-05-19 haftmann 2007-05-19 uniform module names for code generation
2007-05-17 haftmann 2007-05-17 tuned
2007-05-10 haftmann 2007-05-10 tuned
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-26 haftmann 2007-04-26 added lemmatas
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-17 wenzelm 2007-04-17 tuned proofs;
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-02-07 berghofe 2007-02-07 Adapted to changes in Transitive_Closure theory.
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-11-18 haftmann 2006-11-18 div is now a class
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-09-20 haftmann 2006-09-20 name shifts
2006-09-19 haftmann 2006-09-19 explicit divmod algorithm for code generation
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-07-29 webertj 2006-07-29 lin_arith_prover splits certain operators (e.g. min, max, abs)