src/HOL/Library/Permutation.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 17200 3a4d03d1a31b
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     3 *)
     3 *)
     4 
     4 
     5 header {* Permutations *}
     5 header {* Permutations *}
     6 
     6 
     7 theory Permutation
     7 theory Permutation
     8 import Multiset
     8 imports Multiset
     9 begin
     9 begin
    10 
    10 
    11 consts
    11 consts
    12   perm :: "('a list * 'a list) set"
    12   perm :: "('a list * 'a list) set"
    13 
    13