src/HOL/Library/Multiset.thy
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
2009-10-25 wenzelm 2009-10-25 adapted Function_Lib (cf. b8cdd3d73022);
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-28 nipkow 2009-08-28 tuned proofs
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-19 wenzelm 2009-03-19 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-11 haftmann 2009-03-11 explicitly delete some code equations
2009-02-13 nipkow 2009-02-13 finiteness lemmas
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-14 ballarin 2008-12-14 Ported HOL and HOL-Library to new locales.
2008-12-16 krauss 2008-12-16 method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-25 haftmann 2008-07-25 added class preorder
2008-07-15 ballarin 2008-07-15 Removed uses of context element includes.
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-05-07 berghofe 2008-05-07 Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.
2008-04-07 haftmann 2008-04-07 instantiation replacing primitive instance plus overloaded defs; more conservative type arities
2008-02-28 nipkow 2008-02-28 tuned
2008-02-28 wenzelm 2008-02-28 tuned syntax declaration;
2008-02-26 wenzelm 2008-02-26 tuned document; tuned proofs;
2008-02-26 bulwahn 2008-02-26 Added useful general lemmas from the work with the HeapMonad
2008-02-01 nipkow 2008-02-01 modified MCollect syntax
2008-01-30 nipkow 2008-01-30 added multiset comprehension
2008-01-02 kleing 2008-01-02 renamed foldM to fold_mset on general request added Tobias' lemmas on fold_mset (A+B) etc tuned default simp set for fold_mset
2007-12-13 kleing 2007-12-13 removed syntax in locale left_commutative
2007-12-13 haftmann 2007-12-13 changed order in class parameters
2007-12-13 kleing 2007-12-13 a fold operation for multisets + more lemmas
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-30 nipkow 2007-11-30 added {#.,.,...#}