src/HOL/Library/Multiset.thy
12 months ago nipkow 2018-06-07 utilize 'flip'
12 months ago nipkow 2018-06-06 Keep filter input syntax
13 months ago nipkow 2018-05-22 First step to remove nonstandard "[x <- xs. P]" syntax: only input
16 months ago nipkow 2018-02-19 added lemma
17 months ago nipkow 2018-01-10 Manual updates towards conversion of "op" syntax
17 months ago blanchet 2018-01-03 kill old size infrastructure
19 months ago haftmann 2017-11-11 dedicated definition for coprimality
19 months ago haftmann 2017-10-30 generalized some lemmas on multisets
22 months ago blanchet 2017-08-24 tuning (proofs and code)
22 months ago nipkow 2017-08-15 added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
22 months ago nipkow 2017-08-15 added Min_mset and Max_mset
22 months ago nipkow 2017-08-03 tuned
23 months ago eberlm 2017-07-15 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
2017-04-21 blanchet 2017-04-21 moved lemmas from AFP to Isabelle
2017-04-21 blanchet 2017-04-21 two new induction principles on multisets
2017-04-12 haftmann 2017-04-12 tuned
2017-04-03 eberlm 2017-04-03 removed problematic simp rule
2017-04-03 eberlm 2017-04-03 added shuffle product to HOL/List
2017-02-24 blanchet 2017-02-24 added multiset lemma
2017-02-24 blanchet 2017-02-24 added multiset lemma
2017-02-16 fleury 2017-02-16 use the cancellation simprocs directly
2017-02-14 fleury 2017-02-14 cancellation simprocs generalising the multiset simprocs
2017-02-13 fleury 2017-02-13 renaming multiset simprocs
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