--- a/src/HOL/Algebra/AbelCoset.thy Mon Sep 10 21:33:14 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Tue Sep 11 16:21:54 2018 +0100
@@ -403,8 +403,7 @@
by (rule group.rcos_equation [OF a_group a_subgroup,
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
-lemma (in abelian_subgroup) a_rcos_disjoint:
- shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
+lemma (in abelian_subgroup) a_rcos_disjoint: "pairwise disjnt (a_rcosets H)"
by (rule group.rcos_disjoint [OF a_group a_subgroup,
folded A_RCOSETS_def, simplified monoid_record_simps])