diff -r dc6be28d7f4e -r c69542757a4d src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Library/Permutation.thy Mon Aug 16 14:22:27 2004 +0200 @@ -4,7 +4,9 @@ header {* Permutations *} -theory Permutation = Multiset: +theory Permutation +import Multiset +begin consts perm :: "('a list * 'a list) set"