src/HOL/Divides.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)
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-11-18 chaieb 2005-11-18 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-11-11 huffman 2005-11-11 add header
2005-09-23 wenzelm 2005-09-23 Provers/cancel_sums.ML: Simplifier.inherit_bounds;
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-04-22 paulson 2004-04-22 new lemmas
2004-03-05 paulson 2004-03-05 some new results
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-09-26 paulson 2003-09-26 misc tidying
2003-07-24 paulson 2003-07-24 declarations moved from PreList.thy
2003-03-25 berghofe 2003-03-25 New theorems split_div' and mod_div_equality'.
2002-08-23 nipkow 2002-08-23 Added div+mod cancelling simproc
2002-05-31 nipkow 2002-05-31 Now arith can deal with div/mod arbitrary nat numerals.
2002-05-15 nipkow 2002-05-15 Divides.ML -> Divides_lemmas.ML Converted Divides.thy to Isar.