src/HOL/Library/Multiset.thy
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-12-17 haftmann 2016-12-17 standardized notation
2016-12-17 haftmann 2016-12-17 redundant
2016-12-17 haftmann 2016-12-17 renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
2016-11-29 blanchet 2016-11-29 added lemma about 'mult', as suggested by Bertram Felgenhauer
2016-10-27 fleury 2016-10-27 more lemmas
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-07 fleury 2016-10-07 more lemmas
2016-10-07 fleury 2016-10-07 tuning multisets
2016-10-07 fleury 2016-10-07 more lemmas
2016-10-05 fleury 2016-10-05 more multiset simp rules
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-20 eberlm 2016-09-20 Merged
2016-09-19 eberlm 2016-09-19 Additions to permutations (contributed by Lukas Bulwahn)
2016-09-19 fleury 2016-09-19 # after multiset intersection and union symbol
2016-09-18 fleury 2016-09-18 support replicate_mset in multiset simproc
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-09-13 nipkow 2016-09-13 more lemmas
2016-09-12 fleury 2016-09-12 delete looping simp rule
2016-09-10 nipkow 2016-09-10 more simp
2016-09-09 nipkow 2016-09-09 msetsum -> set_mset, msetprod -> prod_mset
2016-09-05 fleury 2016-09-05 tuning multisets; more interpretations
2016-09-05 fleury 2016-09-05 clean argument of simp add
2016-09-05 fleury 2016-09-05 add_mset constructor in multisets
2016-08-14 blanchet 2016-08-14 tuning whitespace in output syntax
2016-08-08 Bertram Felgenhauer 2016-08-08 add monotonicity propertyies of `mult1` and `mult`
2016-07-29 fleury 2016-07-29 more instantiations for multiset
2016-07-25 wenzelm 2016-07-25 merged
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-07-20 fleury 2016-07-20 adding mset_map to the simp rules
2016-07-07 fleury 2016-07-07 more instantiations for multiset
2016-07-07 blanchet 2016-07-07 moved lemmas and locales around (with minor incompatibilities)
2016-07-05 fleury 2016-07-05 instantiate multiset with multiset ordering
2016-07-01 Manuel Eberl 2016-07-01 Tuned multiset lattice
2016-07-01 Manuel Eberl 2016-07-01 Conditionally complete lattice of multisets
2016-06-17 fleury 2016-06-17 normalising multiset theorem names
2016-06-11 haftmann 2016-06-11 boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2016-06-01 eberlm 2016-06-01 Tuned code equations for mappings and PMFs
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-05-12 haftmann 2016-05-12 clarified heading
2016-05-12 haftmann 2016-05-12 a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-03 wenzelm 2016-04-03 isabelle update_cartouches -c -t;
2016-03-18 nipkow 2016-03-18 superfluous premise (noticed by Julian Nagele)
2016-03-08 haftmann 2016-03-08 syntax for multiset membership modelled after syntax for set membership
2016-02-26 haftmann 2016-02-26 more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-18 haftmann 2016-02-18 more theorems
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-20 blanchet 2016-01-20 added 'supset' variants for new '<#' etc. symbols on multisets
2016-01-06 blanchet 2016-01-06 nicer 'Spec_Rules' for size function
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";