equal
deleted
inserted
replaced
5 |
5 |
6 theory Permutations |
6 theory Permutations |
7 imports |
7 imports |
8 "HOL-Library.Multiset" |
8 "HOL-Library.Multiset" |
9 "HOL-Library.Disjoint_Sets" |
9 "HOL-Library.Disjoint_Sets" |
|
10 Transposition |
10 begin |
11 begin |
11 |
12 |
12 subsection \<open>Auxiliary\<close> |
13 subsection \<open>Auxiliary\<close> |
13 |
14 |
14 abbreviation (input) fixpoints :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> 'a set\<close> |
15 abbreviation (input) fixpoints :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> 'a set\<close> |