src/HOL/Divides.thy
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-10-17 haftmann 2015-10-17 qualify some names stemming from internal bootstrap constructions
2015-09-27 haftmann 2015-09-27 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-19 wenzelm 2015-09-19 eliminated suspicious unicode;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-13 haftmann 2015-08-13 qualified adjust_*
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-08 haftmann 2015-07-08 tuned facts
2015-07-08 haftmann 2015-07-08 moved normalization and unit_factor into Main HOL corpus
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
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