src/HOL/Library/Permutation.thy
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/