equal
deleted
inserted
replaced
10 This theory introduces basics about permutations, i.e. almost |
10 This theory introduces basics about permutations, i.e. almost |
11 everywhere fix bijections. But it is by no means complete. |
11 everywhere fix bijections. But it is by no means complete. |
12 Grieviously missing are cycles since these would require more |
12 Grieviously missing are cycles since these would require more |
13 elaboration, e.g. the concept of distinct lists equivalent |
13 elaboration, e.g. the concept of distinct lists equivalent |
14 under rotation, which maybe would also deserve its own theory. |
14 under rotation, which maybe would also deserve its own theory. |
15 But see theory @{text "src/HOL/ex/Perm_Fragments.thy"} for |
15 But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for |
16 fragments on that. |
16 fragments on that. |
17 \<close> |
17 \<close> |
18 |
18 |
19 subsection \<open>Abstract type of permutations\<close> |
19 subsection \<open>Abstract type of permutations\<close> |
20 |
20 |