src/HOL/Library/Multiset.thy
2012-03-29 kuncar 2012-03-29 use qualified names for rsp and rep_eq theorems in quotient_def
2012-03-28 bulwahn 2012-03-28 changing more definitions to quotient_definition
2012-03-28 bulwahn 2012-03-28 using abstract code equations for proofs of code equations in Multiset
2012-03-27 bulwahn 2012-03-27 association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements
2012-03-14 wenzelm 2012-03-14 some proof indentation;
2012-03-02 bulwahn 2012-03-02 adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2012-02-28 wenzelm 2012-02-28 tuned proofs;
2012-02-01 bulwahn 2012-02-01 improving code equations for multisets that violated the distinct AList abstraction
2012-01-17 bulwahn 2012-01-17 renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
2012-01-17 bulwahn 2012-01-17 renamed theory AList to DAList
2012-01-10 bulwahn 2012-01-10 improving code generation for multisets; adding exhaustive quickcheck generators for multisets
2011-12-26 haftmann 2011-12-26 moved theorem requiring multisets from More_List to Multiset
2011-12-14 bulwahn 2011-12-14 adding code attribute to enable evaluation of equality on multisets
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-20 wenzelm 2011-08-20 odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-05-14 haftmann 2011-05-14 use pointfree characterisation for fold_set locale
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-07 haftmann 2010-12-07 name filter operation just filter (c.f. List.filter and list comprehension syntax)
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 haftmann 2010-12-03 lemma multiset_of_rev
2010-11-18 haftmann 2010-11-18 mapper for mulitset type
2010-11-03 haftmann 2010-11-03 added code lemmas for stable parametrized quicksort
2010-11-03 haftmann 2010-11-03 tuned proof
2010-11-02 haftmann 2010-11-02 tuned proof
2010-11-02 haftmann 2010-11-02 tuned proof
2010-11-02 haftmann 2010-11-02 tuned lemma proposition of properties_for_sort_key
2010-11-02 haftmann 2010-11-02 lemmas multiset_of_filter, sort_key_by_quicksort
2010-10-29 Lars Noschinski 2010-10-29 merged
2010-09-22 Lars Noschinski 2010-09-22 Remove unnecessary premise of mult1_union
2010-10-27 haftmann 2010-10-27 sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-09-17 haftmann 2010-09-17 generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
2010-09-14 nipkow 2010-09-14 removed duplicate lemma
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-13 nipkow 2010-09-13 added and renamed lemmas
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-09 blanchet 2010-08-09 replace "setup" with "declaration"
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-06-01 blanchet 2010-06-01 honor xsymbols in Nitpick
2010-05-27 blanchet 2010-05-27 make Nitpick "show_all" option behave less surprisingly
2010-05-24 haftmann 2010-05-24 more lemmas
2010-05-22 haftmann 2010-05-22 localized properties_for_sort
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-05-12 nipkow 2010-05-12 simplified proof
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-11 blanchet 2010-03-11 added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-24 wenzelm 2010-02-24 observe standard convention for syntax consts;
2010-02-23 haftmann 2010-02-23 mind the "s"
2010-02-22 haftmann 2010-02-22 ascii syntax for multiset order
2010-02-19 haftmann 2010-02-19 switched notations for pointwise and multiset order
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-22 haftmann 2010-01-22 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