equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Permutation.thy |
1 (* Title: HOL/Library/Permutation.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson and Thomas M Rasmussen |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 |
5 |
6 TODO: it would be nice to prove (for "multiset", defined on |
6 TODO: it would be nice to prove (for "multiset", defined on |
7 HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x) |
7 HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x) |
8 *) |
8 *) |
9 |
9 |
10 header {* |
10 header {* Permutations *} |
11 \title{Permutations} |
|
12 \author{Lawrence C Paulson and Thomas M Rasmussen} |
|
13 *} |
|
14 |
11 |
15 theory Permutation = Main: |
12 theory Permutation = Main: |
16 |
13 |
17 consts |
14 consts |
18 perm :: "('a list * 'a list) set" |
15 perm :: "('a list * 'a list) set" |