equal
deleted
inserted
replaced
234 proof - |
234 proof - |
235 interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |
235 interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |
236 by (rule a_normal) |
236 by (rule a_normal) |
237 |
237 |
238 show "abelian_subgroup H G" |
238 show "abelian_subgroup H G" |
239 by default (simp add: a_comm) |
239 by standard (simp add: a_comm) |
240 qed |
240 qed |
241 |
241 |
242 lemma abelian_subgroupI2: |
242 lemma abelian_subgroupI2: |
243 fixes G (structure) |
243 fixes G (structure) |
244 assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |
244 assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |