src/HOL/Library/Multiset.thy
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
2005-08-31 wenzelm 2005-08-31 tuned presentation;
2005-08-28 wenzelm 2005-08-28 tuned some proofs;
2005-04-28 kleing 2005-04-28 intersection
2005-04-28 kleing 2005-04-28 some more lemmas about multiset_of
2005-03-26 kleing 2005-03-26 fixed typo (multiset_append) moved multiset_of_complement_union from ex/Sorting
2004-12-12 nipkow 2004-12-12 REorganized Finite_Set
2004-11-23 nipkow 2004-11-23 renamed 1 lemmas
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-22 paulson 2004-07-22 new material courtesy of Norbert Voelker
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-09 obua 2004-05-09 replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-03-08 ballarin 2004-03-08 Bug-fixes for transitivity reasoner.
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-09-30 nipkow 2002-09-30 modified induct method
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.