src/HOL/Library/Multiset.thy
Mon, 26 Dec 2011 22:17:10 +0100 haftmann moved theorem requiring multisets from More_List to Multiset
Wed, 14 Dec 2011 15:56:29 +0100 bulwahn adding code attribute to enable evaluation of equality on multisets
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Sun, 20 Nov 2011 21:28:07 +0100 wenzelm eliminated obsolete "standard";
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Sat, 20 Aug 2011 23:36:18 +0200 wenzelm odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Sat, 14 May 2011 18:26:25 +0200 haftmann use pointfree characterisation for fold_set locale
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Tue, 07 Dec 2010 16:33:54 +0100 haftmann name filter operation just filter (c.f. List.filter and list comprehension syntax)
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemma multiset_of_rev
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mulitset type
Wed, 03 Nov 2010 12:15:47 +0100 haftmann added code lemmas for stable parametrized quicksort
Wed, 03 Nov 2010 11:50:29 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:59:40 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:48:19 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:36:33 +0100 haftmann tuned lemma proposition of properties_for_sort_key
Tue, 02 Nov 2010 16:31:56 +0100 haftmann lemmas multiset_of_filter, sort_key_by_quicksort
Fri, 29 Oct 2010 10:14:49 +0200 Lars Noschinski merged
Wed, 22 Sep 2010 09:56:39 +0200 Lars Noschinski Remove unnecessary premise of mult1_union
Wed, 27 Oct 2010 16:40:31 +0200 haftmann sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
Fri, 17 Sep 2010 20:53:50 +0200 haftmann generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
Tue, 14 Sep 2010 08:40:22 +0200 nipkow removed duplicate lemma
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Mon, 13 Sep 2010 08:43:48 +0200 nipkow added and renamed lemmas
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 09 Aug 2010 12:53:16 +0200 blanchet replace "setup" with "declaration"
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Tue, 01 Jun 2010 14:14:02 +0200 blanchet honor xsymbols in Nitpick
Thu, 27 May 2010 16:42:03 +0200 blanchet make Nitpick "show_all" option behave less surprisingly
Mon, 24 May 2010 13:48:57 +0200 haftmann more lemmas
Sat, 22 May 2010 10:12:49 +0200 haftmann localized properties_for_sort
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Wed, 12 May 2010 15:25:02 +0200 nipkow simplified proof
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Thu, 11 Mar 2010 15:33:45 +0100 blanchet added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
Sat, 27 Feb 2010 20:57:08 +0100 wenzelm clarified @{const_name} vs. @{const_abbrev};
Wed, 24 Feb 2010 21:55:46 +0100 wenzelm observe standard convention for syntax consts;
Tue, 23 Feb 2010 08:08:23 +0100 haftmann mind the "s"
Mon, 22 Feb 2010 09:15:11 +0100 haftmann ascii syntax for multiset order
Fri, 19 Feb 2010 16:52:00 +0100 haftmann switched notations for pointwise and multiset order
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Fri, 22 Jan 2010 13:38:28 +0100 haftmann cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
Sun, 25 Oct 2009 00:00:53 +0200 wenzelm adapted Function_Lib (cf. b8cdd3d73022);
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 28 Aug 2009 19:35:49 +0200 nipkow tuned proofs
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Thu, 19 Mar 2009 22:05:00 +0100 wenzelm proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
Wed, 11 Mar 2009 08:45:46 +0100 haftmann explicitly delete some code equations
Fri, 13 Feb 2009 23:55:04 +0100 nipkow finiteness lemmas
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation
Tue, 30 Dec 2008 11:10:01 +0100 ballarin Merged.
Sun, 14 Dec 2008 18:45:51 +0100 ballarin Ported HOL and HOL-Library to new locales.
less more (0) -100 -60 tip