src/HOL/Library/Permutation.thy
changeset 14706 71590b7733b7
parent 11153 950ede59c05a
child 15005 546c8e7e28d4
     1.1 --- a/src/HOL/Library/Permutation.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,16 +1,13 @@
     1.4  (*  Title:      HOL/Library/Permutation.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author:     Lawrence C Paulson and Thomas M Rasmussen
     1.8      Copyright   1995  University of Cambridge
     1.9  
    1.10  TODO: it would be nice to prove (for "multiset", defined on
    1.11  HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x)
    1.12  *)
    1.13  
    1.14 -header {*
    1.15 - \title{Permutations}
    1.16 - \author{Lawrence C Paulson and Thomas M Rasmussen}
    1.17 -*}
    1.18 +header {* Permutations *}
    1.19  
    1.20  theory Permutation = Main:
    1.21