src/HOL/Rings.thy
Sun, 16 Oct 2016 09:31:03 +0200 haftmann added lemma
Wed, 12 Oct 2016 20:38:47 +0200 haftmann separate type class for arbitrary quotient and remainder partitions
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
Mon, 26 Sep 2016 07:56:54 +0200 haftmann more lemmas
Sun, 18 Sep 2016 17:57:55 +0200 haftmann more generic algebraic lemmas
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Tue, 02 Aug 2016 21:05:34 +0200 wenzelm misc tuning and modernization;
Tue, 12 Jul 2016 13:55:35 +0200 fleury sharing simp rules between ordered monoids and rings
Fri, 01 Jul 2016 08:35:15 +0200 Manuel Eberl More lemmas on Gcd/Lcm
Mon, 20 Jun 2016 21:40:48 +0200 wenzelm misc tuning and modernization;
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Wed, 16 Mar 2016 13:57:06 +0000 paulson Contractible sets. Also removal of obsolete theorems and refactoring
Sun, 13 Mar 2016 10:22:46 +0100 haftmann more theorems on orderings
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Fri, 12 Feb 2016 16:09:07 +0100 hoelzl moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl 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.
Thu, 18 Feb 2016 17:53:09 +0100 haftmann more theorems
Wed, 17 Feb 2016 21:51:57 +0100 haftmann cleansed junk-producing interpretations for gcd/lcm on nat altogether
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 08 Jul 2015 20:19:12 +0200 haftmann tuned facts
Wed, 08 Jul 2015 14:01:41 +0200 haftmann avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
Wed, 08 Jul 2015 14:01:34 +0200 haftmann moved normalization and unit_factor into Main HOL corpus
Tue, 30 Jun 2015 13:56:16 +0100 paulson Useful lemmas. The theorem concerning swapping the variables in a double integral.
Thu, 25 Jun 2015 15:01:42 +0200 haftmann more theorems
Tue, 23 Jun 2015 16:55:28 +0100 paulson 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.
Sat, 20 Jun 2015 15:43:36 +0200 wenzelm avoid suspicious Unicode;
Fri, 19 Jun 2015 07:53:35 +0200 haftmann separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
Fri, 19 Jun 2015 07:53:33 +0200 haftmann generalized some theorems about integral domains and moved to HOL theories
Fri, 12 Jun 2015 08:53:23 +0200 haftmann uniform _ div _ as infix syntax for ring division
Mon, 01 Jun 2015 18:59:22 +0200 haftmann implicit partial divison operation in integral domains
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Thu, 02 Apr 2015 11:22:22 +0200 haftmann semidom contains distributive minus, by convention
Tue, 31 Mar 2015 16:48:48 +0100 paulson rationalised and generalised some theorems concerning abs and x^2.
Sat, 28 Mar 2015 21:32:48 +0100 haftmann clarified no_zero_devisors: makes only sense in a semiring;
Sat, 28 Mar 2015 20:43:19 +0100 haftmann dropped long-outdated comments
Mon, 23 Mar 2015 19:05:14 +0100 haftmann distributivity of partial minus establishes desired properties of dvd in semirings
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Wed, 18 Feb 2015 22:46:48 +0100 haftmann eliminated fact duplicates
Sat, 14 Feb 2015 10:24:15 +0100 haftmann fact consolidation
Mon, 17 Nov 2014 14:55:33 +0100 haftmann generalized lemmas (particularly concerning dvd) as far as appropriate
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sat, 08 Nov 2014 16:53:26 +0100 haftmann equivalence rules for structures without zero divisors
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 24 Oct 2014 15:07:51 +0200 hoelzl use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
Sun, 12 Oct 2014 17:05:34 +0200 haftmann generalized and consolidated some theorems concerning divisibility
Sun, 12 Oct 2014 16:31:28 +0200 haftmann more facts about abstract divisibility
Sun, 07 Sep 2014 09:49:01 +0200 haftmann generalized
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
less more (0) -60 tip