src/HOL/Divides.thy
2017-04-23 haftmann 2017-04-23 more lemmas
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
2017-01-04 haftmann 2017-01-04 moved euclidean ring to HOL
2016-12-31 haftmann 2016-12-31 more elementary rules about div / mod on int
2016-12-22 haftmann 2016-12-22 more uniform div/mod relations
2016-12-20 haftmann 2016-12-20 emphasize dedicated rewrite rules for congruences
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-10-16 haftmann 2016-10-16 clarified prover-specific rules
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 clarified theorem names
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-10-16 haftmann 2016-10-16 more standardized names
2016-10-16 haftmann 2016-10-16 de-orphanized declaration
2016-10-12 haftmann 2016-10-12 separate type class for arbitrary quotient and remainder partitions
2016-10-03 haftmann 2016-10-03 more lemmas
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-26 haftmann 2016-09-26 more lemmas
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-07-14 eberlm 2016-07-14 Tuned looping simp rules in semiring_div
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-02-23 nipkow 2016-02-23 more canonical names
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