changeset 2560 | 82e37a4595c7 |
parent 2507 | f5621efe5a20 |
child 2565 | 6bf332360510 |
--- a/Nominal-General/Nominal2_Base.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal-General/Nominal2_Base.thy Fri Nov 12 01:20:53 2010 +0000 @@ -142,6 +142,7 @@ "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2" by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) +instance perm :: size .. subsection {* Permutations form a group *}