| changeset 30738 | 0842e906300c |
| parent 27368 | 9f90ac19e32b |
| child 30742 | 3e89ac3905b9 |
| 30737:9ffd27558916 | 30738:0842e906300c |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Permutations *} |
5 header {* Permutations *} |
6 |
6 |
7 theory Permutation |
7 theory Permutation |
8 imports Plain Multiset |
8 imports Main 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 |