# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1677583187 0
# Node ID 02af8a1b97f6cbd660d2a81188681e59c083b716
# Parent  c2013f617a7081d1aa9f213a7fb0ebd9a925583c
Fixed a presentation error

diff -r c2013f617a70 -r 02af8a1b97f6 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Feb 27 17:09:59 2023 +0000
+++ b/src/HOL/Algebra/Coset.thy	Tue Feb 28 11:19:47 2023 +0000
@@ -1609,7 +1609,7 @@
   shows "H <#> N = H"
   using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp
 
-text \<open>A normal subgroup is commutative with set_mult\<close>
+text \<open>A normal subgroup is commutative with set multiplication\<close>
 lemma (in group) commut_normal:
   assumes "subgroup H G" and "N\<lhd>G"
   shows "H<#>N = N<#>H"