src/HOL/Library/Multiset.thy
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 {#.,.,...#}
2007-10-26 haftmann 2007-10-26 changed order of class parameters
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-21 nipkow 2007-10-21 More changes from >0 to ~=0::nat
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-07-29 wenzelm 2007-07-29 simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";
2007-07-11 berghofe 2007-07-11 Restored set notation.
2007-07-06 nipkow 2007-07-06 more interpretations
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-06 nipkow 2007-06-06 changed filter syntax from : to <-
2007-02-14 haftmann 2007-02-14 added class "preorder"
2007-02-07 berghofe 2007-02-07 Converted to predicate notation.
2006-11-18 haftmann 2006-11-18 using class instance
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 haftmann 2006-11-07 adjusted two lemma names due to name change in interpretation
2006-09-28 wenzelm 2006-09-28 fixed translations: CONST;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-05-05 wenzelm 2006-05-05 get rid of 'concl is';
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2006-01-21 wenzelm 2006-01-21 tuned proofs;
2005-11-25 wenzelm 2005-11-25 tuned induct proofs;
2005-10-07 nipkow 2005-10-07 changes due to new neq_simproc in simpdata.ML