src/HOL/Rings.thy
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
2014-10-12 haftmann 2014-10-12 more facts about abstract divisibility
2014-09-07 haftmann 2014-09-07 generalized
2014-09-06 haftmann 2014-09-06 added various facts
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-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-04 huffman 2014-03-04 fix typo
2014-01-30 haftmann 2014-01-30 split rules for of_bool, similar to if
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 generalized of_bool conversion
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
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-03-26 hoelzl 2013-03-26 move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2012-12-07 nipkow 2012-12-07 corrected nonsensical associativity of `` and dvd
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-09-13 huffman 2011-09-13 tuned proofs