src/HOL/Divides.thy
2015-06-19 haftmann 2015-06-19 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
2015-06-19 haftmann 2015-06-19 generalized some theorems about integral domains and moved to HOL theories
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 implicit partial divison operation in integral domains
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-03-28 haftmann 2015-03-28 clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-02-18 haftmann 2015-02-18 eliminated technical fact alias
2015-01-30 nipkow 2015-01-30 canonical name
2015-01-16 nipkow 2015-01-16 added simp lemma
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-17 haftmann 2014-11-17 generalized lemmas (particularly concerning dvd) as far as appropriate
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-09 haftmann 2014-11-09 self-contained simp rules for dvd on numerals
2014-11-05 haftmann 2014-11-05 proper oriented equivalence of dvd predicate and mod
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-31 wenzelm 2014-10-31 avoid noise (cf. 03ff4d1e6784);
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