src/HOL/Library/Permutation.thy
2016-12-17 haftmann 2016-12-17 standardized notation
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-06-17 fleury 2016-06-17 normalising multiset theorem names
2015-11-18 paulson 2015-11-18 New theorems mostly from Peter Gammie
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-06-19 nipkow 2015-06-19 renamed multiset_of -> mset
2015-06-17 wenzelm 2015-06-17 manual merge;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-17 nipkow 2015-06-17 renamed Multiset.set_of to the canonical set_mset
2015-06-10 Mathias Fleury 2015-06-10 Renaming multiset operators < ~> <#,...
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-04-29 wenzelm 2014-04-29 tuned proofs;
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
2013-08-27 wenzelm 2013-08-27 tuned proofs;
2013-03-26 wenzelm 2013-03-26 tuned imports;
2012-11-08 bulwahn 2012-11-08 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2010-10-25 haftmann 2010-10-25 dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-04 haftmann 2010-10-04 turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-09-02 hoelzl 2010-09-02 Fixes lemma names
2010-09-02 hoelzl 2010-09-02 Permutation implies bij function
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-02-22 haftmann 2010-02-22 switched notations for pointwise and multiset order
2009-11-07 haftmann 2009-11-07 modernized primrec
2009-03-27 haftmann 2009-03-27 tuned notoriously slow metis proof
2009-03-27 haftmann 2009-03-27 normalized imports
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-18 wenzelm 2008-03-18 removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2007-11-10 wenzelm 2007-11-10 tuned proofs; tuned document;
2007-11-05 nipkow 2007-11-05 added lemmas
2007-11-05 nipkow 2007-11-05 added lemmas
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2005-08-31 wenzelm 2005-08-31 tuned presentation;
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-24 paulson 2004-06-24 Norbert Voelker
2004-05-06 wenzelm 2004-05-06 tuned document;
2001-02-16 paulson 2001-02-16 Blast bug fix made old proof too slow
2001-02-04 wenzelm 2001-02-04 moved from Induct/ to Library/