| changeset 15131 | c69542757a4d |
| parent 15072 | 4861bf6af0b4 |
| child 15140 | 322485b816ac |
| 15130:dc6be28d7f4e | 15131:c69542757a4d |
|---|---|
2 Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
2 Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
3 *) |
3 *) |
4 |
4 |
5 header {* Permutations *} |
5 header {* Permutations *} |
6 |
6 |
7 theory Permutation = Multiset: |
7 theory Permutation |
8 import Multiset |
|
9 begin |
|
8 |
10 |
9 consts |
11 consts |
10 perm :: "('a list * 'a list) set" |
12 perm :: "('a list * 'a list) set" |
11 |
13 |
12 syntax |
14 syntax |