src/HOL/Library/Multiset.thy
4 months ago wenzelm 2019-03-10 more formal contributors (with the help of the history);
6 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
7 months ago wenzelm 2018-12-10 tuned proofs;
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
9 months ago nipkow 2018-10-03 shuffle -> shuffles
10 months ago nipkow 2018-09-23 use standard syntax
10 months ago nipkow 2018-09-14 tuned
10 months ago nipkow 2018-09-13 removed redundant lemma
10 months ago nipkow 2018-09-13 more simp lemmas
10 months ago nipkow 2018-09-13 prefer explicit
10 months ago nipkow 2018-09-13 typo
10 months ago nipkow 2018-09-12 added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
10 months ago haftmann 2018-09-08 left-over rename from 3f9bb52082c4
13 months ago nipkow 2018-06-07 utilize 'flip'
13 months ago nipkow 2018-06-06 Keep filter input syntax
14 months ago nipkow 2018-05-22 First step to remove nonstandard "[x <- xs. P]" syntax: only input
17 months ago nipkow 2018-02-19 added lemma
18 months ago nipkow 2018-01-10 Manual updates towards conversion of "op" syntax
18 months ago blanchet 2018-01-03 kill old size infrastructure
20 months ago haftmann 2017-11-11 dedicated definition for coprimality
21 months ago haftmann 2017-10-30 generalized some lemmas on multisets
23 months ago blanchet 2017-08-24 tuning (proofs and code)
23 months ago nipkow 2017-08-15 added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
23 months ago nipkow 2017-08-15 added Min_mset and Max_mset
23 months ago nipkow 2017-08-03 tuned
2017-07-15 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