src/HOL/Divides.thy
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.
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-01-05 nipkow 2001-01-05 Changed priority of dvd from 70 to 50 as befits a relation.
2000-12-01 paulson 2000-12-01 many new div and mod properties (borrowed from Integ/IntDiv)
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-05-24 paulson 2000-05-24 installing plus_ac0 for nat
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
1999-07-19 paulson 1999-07-19 new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
1999-07-01 paulson 1999-07-01 now div and mod are overloaded; dvd is polymorphic
1997-05-30 paulson 1997-05-30 Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides