src/HOL/Rings.thy
Tue, 22 May 2018 18:14:29 +0000 haftmann consider dvdE for automated classical proving
Thu, 22 Feb 2018 22:58:27 +0000 paulson type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
Thu, 21 Dec 2017 08:23:19 +0100 eberlm Some lemmas on complex numbers and coprimality
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 23 Nov 2017 17:03:20 +0000 haftmann tuned
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Mon, 30 Oct 2017 13:18:44 +0000 haftmann rule out pathologic instances
Sun, 08 Oct 2017 22:28:22 +0200 haftmann more fundamental definition of div and mod on int
Sun, 08 Oct 2017 22:28:21 +0200 haftmann generalized simproc
Sun, 08 Oct 2017 22:28:21 +0200 haftmann elementary definition of division on natural numbers
Sun, 08 Oct 2017 22:28:21 +0200 haftmann tuned structure
Mon, 09 Oct 2017 15:34:23 +0100 paulson new material about connectedness, etc.
Thu, 11 May 2017 16:47:53 +0200 haftmann more lemmas
Mon, 09 Jan 2017 18:53:06 +0100 haftmann slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
Fri, 30 Dec 2016 18:02:27 +0100 haftmann more facts on sgn, abs
Sat, 17 Dec 2016 15:22:14 +0100 haftmann more fine-grained type class hierarchy for div and mod
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Tue, 18 Oct 2016 18:48:53 +0200 haftmann suitable logical type class for abs, sgn
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
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
less more (0) -100 -60 tip