src/HOL/Library/Multiset.thy
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.
Thu, 18 Feb 2016 17:53:09 +0100 haftmann more theorems
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Wed, 20 Jan 2016 17:14:53 +0100 blanchet added 'supset' variants for new '<#' etc. symbols on multisets
Wed, 06 Jan 2016 13:04:31 +0100 blanchet nicer 'Spec_Rules' for size function
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Sat, 19 Dec 2015 11:05:04 +0100 haftmann abandoned attempt to unify sublocale and interpretation into global theories
Sat, 12 Dec 2015 16:32:00 +0100 haftmann modernized
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Tue, 06 Oct 2015 17:44:32 +0200 wenzelm merged
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Tue, 06 Oct 2015 11:50:23 +0200 blanchet compile
Thu, 17 Sep 2015 15:47:24 +0200 wenzelm isabelle update_cartouches;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Thu, 27 Aug 2015 13:07:45 +0200 haftmann more lemmas on sorting and multisets (due to Thomas Sewell)
Mon, 27 Jul 2015 22:44:02 +0200 haftmann formal class for factorial (semi)rings
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Mon, 06 Jul 2015 22:06:02 +0200 wenzelm tuned proofs;
Tue, 30 Jun 2015 13:29:30 +0200 hoelzl fix tex-output for rel_mset
Mon, 29 Jun 2015 16:07:55 +0200 wenzelm tuned proofs;
Mon, 29 Jun 2015 15:41:16 +0200 wenzelm more symbols;
Mon, 29 Jun 2015 15:36:29 +0200 wenzelm more symbols;
Fri, 19 Jun 2015 15:55:22 +0200 nipkow renamed multiset_of -> mset
Thu, 18 Jun 2015 16:16:17 +0200 nipkow multiset_of_set -> mset_set
Wed, 17 Jun 2015 18:22:29 +0200 wenzelm merged
Wed, 17 Jun 2015 17:54:09 +0200 wenzelm manual merge;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Wed, 17 Jun 2015 18:13:44 +0200 nipkow more compact name
Wed, 17 Jun 2015 17:21:11 +0200 nipkow renamed Multiset.set_of to the canonical set_mset
Wed, 10 Jun 2015 15:50:17 +0200 fleury tuned
Wed, 10 Jun 2015 13:24:16 +0200 Mathias Fleury Renaming multiset operators < ~> <#,...
Fri, 10 Apr 2015 12:16:58 +0200 nipkow merged
Fri, 10 Apr 2015 12:16:45 +0200 nipkow renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
Fri, 10 Apr 2015 11:52:55 +0200 wenzelm tuned proofs;
Thu, 09 Apr 2015 18:00:58 +0200 blanchet introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
Wed, 08 Apr 2015 15:21:20 +0200 blanchet renamed multiset ordering to free up nice <# etc. symbols for the standard subset
Tue, 07 Apr 2015 18:21:56 +0200 nipkow Removed mcard because it is equal to size
Mon, 23 Mar 2015 19:05:14 +0100 haftmann explicit commutative additive inverse operation;
Wed, 25 Mar 2015 17:51:34 +0100 blanchet more multiset theorems
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Fri, 06 Mar 2015 20:08:45 +0100 wenzelm proper context;
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Wed, 24 Sep 2014 15:45:55 +0200 blanchet simpler proof
Tue, 09 Sep 2014 17:50:54 +0200 nipkow enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
Sat, 30 Aug 2014 11:15:47 +0200 haftmann inlined unused definition
Fri, 22 Aug 2014 17:35:48 +0200 blanchet added lemmas contributed by Rene Thiemann
Sun, 17 Aug 2014 22:27:58 +0200 blanchet use 'image_mset' as BNF map function
Sat, 05 Jul 2014 16:04:23 +0200 haftmann refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
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
less more (0) -100 -60 tip