src/HOL/Algebra/Group.thy
 changeset 19984 29bb4659f80a parent 19981 c0f124a0d385 child 20318 0e0ea63fe768
equal inserted replaced
19983:d649506f40c3 19984:29bb4659f80a
`   656 `
`   656 `
`   657 lemma (in group) group_comm_groupI:`
`   657 lemma (in group) group_comm_groupI:`
`   658   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>`
`   658   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>`
`   659       x \<otimes> y = y \<otimes> x"`
`   659       x \<otimes> y = y \<otimes> x"`
`   660   shows "comm_group G"`
`   660   shows "comm_group G"`
`   661   by intro_locales (simp_all add: m_comm)`
`   661   by unfold_locales (simp_all add: m_comm)`
`   662 `
`   662 `
`   663 lemma comm_groupI:`
`   663 lemma comm_groupI:`
`   664   fixes G (structure)`
`   664   fixes G (structure)`
`   665   assumes m_closed:`
`   665   assumes m_closed:`
`   666       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"`
`   666       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"`