equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 section \<open>Permutations as abstract type\<close> |
3 section \<open>Permutations as abstract type\<close> |
4 |
4 |
5 theory Perm |
5 theory Perm |
6 imports Main |
6 imports |
|
7 Transposition |
7 begin |
8 begin |
8 |
9 |
9 text \<open> |
10 text \<open> |
10 This theory introduces basics about permutations, i.e. almost |
11 This theory introduces basics about permutations, i.e. almost |
11 everywhere fix bijections. But it is by no means complete. |
12 everywhere fix bijections. But it is by no means complete. |