src/HOL/Library/Permutation.thy
changeset 51542 738598beeb26
parent 50037 f2a32197a33a
child 53238 01ef0a103fc9
equal deleted inserted replaced
51541:e7b6b61b7be2 51542:738598beeb26
     3 *)
     3 *)
     4 
     4 
     5 header {* Permutations *}
     5 header {* Permutations *}
     6 
     6 
     7 theory Permutation
     7 theory Permutation
     8 imports Main Multiset
     8 imports Multiset
     9 begin
     9 begin
    10 
    10 
    11 inductive
    11 inductive
    12   perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
    12   perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
    13   where
    13   where