src/HOL/Groups_Big.thy
Tue, 06 Apr 2021 18:12:20 +0000 haftmann new lemmas
Wed, 05 Aug 2020 17:56:33 +0100 paulson yet another little lemma
Fri, 31 Jul 2020 12:54:46 +0100 paulson A new lemma about abstract Sum / Prod
Thu, 09 Jan 2020 08:42:01 +0100 nipkow added lemma
Wed, 18 Sep 2019 14:41:37 +0100 paulson imported new material mostly due to Sébastien Gouëzel
Thu, 11 Apr 2019 17:16:03 +0100 paulson merge plus tidied three proofs
Wed, 10 Apr 2019 13:34:55 +0100 paulson The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
Thu, 04 Apr 2019 16:38:45 +0100 paulson fixed markup in Poly_Mapping; Free_Abelian_Groups (but not yet imported by Algebra!)
Thu, 04 Apr 2019 14:19:33 +0100 paulson More group theory. Sum and product indexed by the non-neutral part of a set
Wed, 13 Feb 2019 09:50:16 +0100 nipkow removed subsumed lemma
Thu, 31 Jan 2019 09:30:15 +0100 nipkow less special syntax: make \<Sum> an ordinary function symbol
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Mon, 14 Jan 2019 14:46:12 +0100 nipkow uniform naming
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 27 Dec 2018 21:00:50 +0100 immler generalized to big sum
Mon, 19 Nov 2018 13:40:04 +0100 nipkow Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Sun, 21 Oct 2018 09:39:09 +0200 nipkow uniform naming of strong congruence rules
Wed, 17 Oct 2018 14:19:07 +0100 paulson new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
Sat, 06 Oct 2018 08:59:05 +0200 nipkow generalization due to Alexander Maletzky
Tue, 11 Sep 2018 16:21:54 +0100 paulson A few new results, elimination of duplicates and more use of "pairwise"
Sun, 03 Jun 2018 15:22:30 +0100 paulson infinite product material
Mon, 09 Apr 2018 15:20:11 +0100 paulson Syntax for the special cases Min(A`I) and Max (A`I)
Wed, 21 Feb 2018 12:57:49 +0000 paulson Lots of new material about matrices, etc.
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Sat, 27 Jan 2018 10:27:57 +0100 bulwahn include lemmas generally useful for combinatorial proofs
Fri, 22 Dec 2017 21:00:07 +0000 paulson new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Sun, 08 Oct 2017 22:28:20 +0200 haftmann avoid name clashes on interpretation of abstract locales
Mon, 07 Aug 2017 11:21:11 +0200 blanchet tuning imports
Mon, 19 Jun 2017 16:07:47 +0100 paulson New theorems; stronger theorems; tidier theorems. Also some renaming
Thu, 15 Jun 2017 17:22:23 +0100 paulson Some new material. SIMPRULE STATUS for sum/prod.delta rules!
Wed, 03 May 2017 14:39:04 +0100 paulson two new theorems
Tue, 02 May 2017 14:34:06 +0100 paulson Simplification of some proofs. Also key lemmas using !! rather than ! in premises
Thu, 02 Feb 2017 09:55:16 -0500 hoelzl move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Thu, 22 Sep 2016 15:44:47 +0100 paulson More mainly topological results
Sun, 18 Sep 2016 17:57:55 +0200 haftmann more generic algebraic lemmas
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
Wed, 10 Aug 2016 22:05:36 +0200 wenzelm misc tuning and modernization;
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Sun, 26 Jun 2016 01:03:03 +0200 nipkow added fundef_cong rule
Sat, 11 Jun 2016 16:22:42 +0200 haftmann boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
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.
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Sun, 27 Dec 2015 22:07:17 +0100 wenzelm discontinued ASCII replacement syntax <*>;
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 02 Dec 2015 19:14:57 +0100 haftmann modernized
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
less more (0) -60 tip