src/HOL/Divides.thy
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-30 haftmann 2014-01-30 more direct simplification rules for 1 div/mod numeral; added simplification rules for (- 1) div/mod numeral
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger
2013-10-31 haftmann 2013-10-31 explicit type class for modelling even/odd parity
2013-10-31 haftmann 2013-10-31 more lemmas on division
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-26 wenzelm 2013-08-26 removed junk;
2013-08-18 haftmann 2013-08-18 spelling and typos
2013-08-18 haftmann 2013-08-18 execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
2013-08-18 haftmann 2013-08-18 relaxed preconditions
2013-08-18 haftmann 2013-08-18 type class for generic division algorithm on numerals
2013-08-18 haftmann 2013-08-18 added lemma
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-19 noschinl 2013-06-19 added lemma
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-02-28 wenzelm 2013-02-28 proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes
2012-12-07 wenzelm 2012-12-07 avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-27 huffman 2012-07-27 move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
2012-04-02 huffman 2012-04-02 add simp rules for dvd on negative numerals
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-27 huffman 2012-03-27 remove more redundant lemmas
2012-03-27 huffman 2012-03-27 tuned proofs
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 generalized lemma zpower_zmod
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-27 huffman 2012-03-27 remove redundant lemma
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