src/HOL/Rings.thy
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
2016-12-30 haftmann 2016-12-30 more facts on sgn, abs
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-18 haftmann 2016-10-18 suitable logical type class for abs, sgn
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 added lemma
2016-10-12 haftmann 2016-10-12 separate type class for arbitrary quotient and remainder partitions
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-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-07-12 fleury 2016-07-12 sharing simp rules between ordered monoids and rings
2016-07-01 Manuel Eberl 2016-07-01 More lemmas on Gcd/Lcm
2016-06-20 wenzelm 2016-06-20 misc tuning and modernization;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-16 paulson 2016-03-16 Contractible sets. Also removal of obsolete theorems and refactoring
2016-03-13 haftmann 2016-03-13 more theorems on orderings
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-12 hoelzl 2016-02-12 moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-18 haftmann 2016-02-18 more theorems
2016-02-17 haftmann 2016-02-17 cleansed junk-producing interpretations for gcd/lcm on nat altogether
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
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 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-08 haftmann 2015-07-08 moved normalization and unit_factor into Main HOL corpus
2015-06-30 paulson 2015-06-30 Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-06-25 haftmann 2015-06-25 more theorems
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-20 wenzelm 2015-06-20 avoid suspicious Unicode;
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-04-02 haftmann 2015-04-02 semidom contains distributive minus, by convention
2015-03-31 paulson 2015-03-31 rationalised and generalised some theorems concerning abs and x^2.
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-28 haftmann 2015-03-28 dropped long-outdated comments
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 eliminated fact duplicates
2015-02-14 haftmann 2015-02-14 fact consolidation
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-08 haftmann 2014-11-08 equivalence rules for structures without zero divisors
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-12 haftmann 2014-10-12 generalized and consolidated some theorems concerning divisibility