src/HOL/Library/Multiset.thy
Fri, 24 Feb 2017 13:59:50 +0100 blanchet added multiset lemma
Fri, 24 Feb 2017 13:59:49 +0100 blanchet added multiset lemma
Thu, 16 Feb 2017 13:54:22 +0100 fleury use the cancellation simprocs directly
Tue, 14 Feb 2017 18:32:53 +0100 fleury cancellation simprocs generalising the multiset simprocs
Mon, 13 Feb 2017 16:03:53 +0100 fleury renaming multiset simprocs
Tue, 17 Jan 2017 13:59:10 +0100 wenzelm isabelle update_cartouches -c -t;
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Sat, 17 Dec 2016 15:22:13 +0100 haftmann standardized notation
Sat, 17 Dec 2016 15:22:00 +0100 haftmann redundant
Sat, 17 Dec 2016 15:22:00 +0100 haftmann renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
Tue, 29 Nov 2016 08:32:44 +0100 blanchet added lemma about 'mult', as suggested by Bertram Felgenhauer
Thu, 27 Oct 2016 15:51:54 +0200 fleury more lemmas
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 07 Oct 2016 17:59:19 +0200 fleury more lemmas
Fri, 07 Oct 2016 17:58:36 +0200 fleury tuning multisets
Fri, 07 Oct 2016 17:57:17 +0200 fleury more lemmas
Wed, 05 Oct 2016 20:12:56 +0200 fleury more multiset simp rules
Sun, 18 Sep 2016 17:57:55 +0200 haftmann more generic algebraic lemmas
Tue, 20 Sep 2016 11:35:10 +0200 eberlm Merged
Mon, 19 Sep 2016 17:37:22 +0200 eberlm Additions to permutations (contributed by Lukas Bulwahn)
Mon, 19 Sep 2016 20:07:39 +0200 fleury # after multiset intersection and union symbol
Sun, 18 Sep 2016 11:31:19 +0200 fleury support replicate_mset in multiset simproc
Thu, 15 Sep 2016 11:48:20 +0200 nipkow renamed listsum -> sum_list, listprod ~> prod_list
Tue, 13 Sep 2016 07:59:20 +0200 nipkow more lemmas
Mon, 12 Sep 2016 08:23:59 +0200 fleury delete looping simp rule
Sat, 10 Sep 2016 14:11:04 +0200 nipkow more simp
Fri, 09 Sep 2016 15:12:40 +0200 nipkow msetsum -> set_mset, msetprod -> prod_mset
Mon, 05 Sep 2016 15:47:50 +0200 fleury tuning multisets; more interpretations
Mon, 05 Sep 2016 15:47:50 +0200 fleury clean argument of simp add
Mon, 05 Sep 2016 15:47:50 +0200 fleury add_mset constructor in multisets
Sun, 14 Aug 2016 12:26:09 +0200 blanchet tuning whitespace in output syntax
Mon, 08 Aug 2016 14:01:49 +0200 Bertram Felgenhauer add monotonicity propertyies of `mult1` and `mult`
Fri, 29 Jul 2016 08:22:59 +0200 fleury more instantiations for multiset
Mon, 25 Jul 2016 11:30:31 +0200 wenzelm merged
Fri, 22 Jul 2016 11:00:43 +0200 wenzelm tuned proofs -- avoid unstructured calculation;
Fri, 22 Jul 2016 08:02:37 +0200 wenzelm tuned proofs -- avoid improper use of "this";
Thu, 21 Jul 2016 10:06:04 +0200 eberlm Overhaul of prime/multiplicity/prime_factors
Wed, 20 Jul 2016 13:51:38 +0200 fleury adding mset_map to the simp rules
Thu, 07 Jul 2016 17:34:39 +0200 fleury more instantiations for multiset
Thu, 07 Jul 2016 09:24:03 +0200 blanchet moved lemmas and locales around (with minor incompatibilities)
Tue, 05 Jul 2016 13:05:04 +0200 fleury instantiate multiset with multiset ordering
Fri, 01 Jul 2016 10:56:54 +0200 Manuel Eberl Tuned multiset lattice
Fri, 01 Jul 2016 08:19:53 +0200 Manuel Eberl Conditionally complete lattice of multisets
Fri, 17 Jun 2016 12:37:43 +0200 fleury normalising multiset theorem names
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
Wed, 01 Jun 2016 13:48:34 +0200 eberlm Tuned code equations for mappings and PMFs
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Thu, 12 May 2016 14:38:53 +0200 haftmann clarified heading
Thu, 12 May 2016 09:34:07 +0200 haftmann a quasi-recursive characterization of the multiset order (by Christian Sternagel)
Tue, 26 Apr 2016 22:44:31 +0200 wenzelm some uses of 'obtain' with structure statement;
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Sun, 03 Apr 2016 23:03:30 +0200 wenzelm isabelle update_cartouches -c -t;
Fri, 18 Mar 2016 12:48:00 +0100 nipkow superfluous premise (noticed by Julian Nagele)
Tue, 08 Mar 2016 21:07:46 +0100 haftmann syntax for multiset membership modelled after syntax for set membership
Fri, 26 Feb 2016 22:44:11 +0100 haftmann more succint formulation of membership for multisets, similar to lists;
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
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.
less more (0) -100 -60 tip