src/HOL/Rings.thy
Wed, 07 Apr 2021 15:46:06 +0000 haftmann subclass relation
Tue, 06 Apr 2021 18:12:20 +0000 haftmann new lemmas
Mon, 06 Apr 2020 19:46:38 +0100 paulson a few more applys
Sun, 05 Apr 2020 22:04:19 +0100 paulson fixed more nasty proofs
Tue, 21 Jan 2020 11:02:27 +0100 Manuel Eberl Removed multiplicativity assumption from normalization_semidom
Tue, 26 Nov 2019 14:32:08 +0000 paulson Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
Sat, 19 Oct 2019 09:15:37 +0000 haftmann generalized
Wed, 09 Oct 2019 14:51:54 +0000 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
Fri, 14 Jun 2019 08:34:28 +0000 haftmann official fact collection sign_simps
Tue, 16 Apr 2019 19:50:21 +0000 haftmann removed unused fact collections
Sat, 13 Apr 2019 08:43:33 +0000 haftmann backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
Sat, 13 Apr 2019 08:11:48 +0000 haftmann tuned
Sat, 13 Apr 2019 08:11:47 +0000 haftmann more document structure
Sat, 13 Apr 2019 08:11:46 +0000 haftmann tuned
Tue, 09 Apr 2019 16:59:00 +0000 haftmann common type class for distributive division
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 23 May 2018 07:13:11 +0000 haftmann grouped material on numeral division
Tue, 22 May 2018 18:14:29 +0000 haftmann automatic classical rule to derive a dvd b from b mod a = 0
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
less more (0) -100 -60 tip