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