src/HOL/Divides.thy
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-25 haftmann 2014-10-25 more simp rules; slight proof tuning
2014-10-23 haftmann 2014-10-23 even further downshift of theory Parity in the hierarchy
2014-10-20 haftmann 2014-10-20 augmented and tuned facts on even/odd and division
2014-10-10 haftmann 2014-10-10 specialized specification: avoid trivial instances
2014-10-02 haftmann 2014-10-02 redundant: dropped
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-02-12 wenzelm 2014-02-12 merged, resolving some conflicts;
2014-02-12 wenzelm 2014-02-12 eliminated hard tabs (assuming tab-width=2);
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)