equal
deleted
inserted
replaced
18 |
18 |
19 subsection \<open>Abstract type of permutations\<close> |
19 subsection \<open>Abstract type of permutations\<close> |
20 |
20 |
21 typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}" |
21 typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}" |
22 morphisms "apply" Perm |
22 morphisms "apply" Perm |
23 by (rule exI [of _ id]) simp |
23 proof |
|
24 show "id \<in> ?perm" by simp |
|
25 qed |
24 |
26 |
25 setup_lifting type_definition_perm |
27 setup_lifting type_definition_perm |
26 |
28 |
27 notation "apply" (infixl "\<langle>$\<rangle>" 999) |
29 notation "apply" (infixl "\<langle>$\<rangle>" 999) |
28 no_notation "apply" ("op \<langle>$\<rangle>") |
30 no_notation "apply" ("op \<langle>$\<rangle>") |