src/HOL/Library/Permutations.thy
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-04-01 wenzelm 2017-04-01 misc tuning and modernization;
2017-01-29 wenzelm 2017-01-29 added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
2016-12-08 bulwahn 2016-12-08 remove typo in bij_swap_compose_bij theorem name; tune proof
2016-10-18 hoelzl 2016-10-18 HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-19 eberlm 2016-09-19 Additions to permutations (contributed by Lukas Bulwahn)
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-05-25 wenzelm 2016-05-25 updated 'define';
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-02-23 nipkow 2016-02-23 more canonical names
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-06-28 nipkow 2015-06-28 added lemma
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 paulson 2015-03-10 renaming HOL/Fact.thy -> Binomial.thy
2015-01-30 hoelzl 2015-01-30 related permutations with bij functions
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-04-16 haftmann 2014-04-16 more simp rules for Fun.swap
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2013-12-06 wenzelm 2013-12-06 tuned proofs;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2011-12-20 bulwahn 2011-12-20 tuned
2011-08-16 huffman 2011-08-16 get Library/Permutations.thy compiled and working again
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-04-25 huffman 2010-04-25 fix duplicate simp rule warnings
2010-04-24 huffman 2010-04-24 fix imports
2009-12-16 huffman 2009-12-16 swap_self already declared [simp]
2009-11-16 hoelzl 2009-11-16 removed hassize predicate
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-12 huffman 2009-03-12 remove trailing spaces
2009-03-04 wenzelm 2009-03-04 removed old/broken CVS Ids;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 huffman 2009-02-23 explicitly import Fact
2009-02-20 huffman 2009-02-20 generalize lemmas from nat to 'a::wellorder
2009-02-20 huffman 2009-02-20 generalize some lemmas
2009-02-09 chaieb 2009-02-09 Permutations, both general and specifically on finite sets.