src/ZF/ex/Group.thy

 
 locale group = monoid +
   assumes inv_ex:
      "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
 
-lemma (in group) is_group [simp]: "group(G)" by fact
+lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)
 
 theorem groupI:
   includes struct G
   assumes m_closed [simp]:
       "\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"

 lemma (in subgroup) subgroup_in_rcosets:
   includes group G
   shows "H \<in> rcosets H"
 proof -
   have "H #> \<one> = H"
-    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
+    using _ subgroup_axioms by (rule coset_join2) simp_all
   then show ?thesis
     by (auto simp add: RCOSETS_def intro: sym)
 qed
 
 lemma (in normal) rcosets_inv_mult_group_eq: