src/HOL/Algebra/Group.thy
changeset 23350 50c5b0912a0c
parent 22063 717425609192
child 26199 04817a8802f2
--- a/src/HOL/Algebra/Group.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -195,7 +195,7 @@
   assumes Units: "carrier G <= Units G"
 
 
-lemma (in group) is_group: "group G" .
+lemma (in group) is_group: "group G" by fact
 
 theorem groupI:
   fixes G (structure)
@@ -383,7 +383,7 @@
     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
 
 lemma (in subgroup) is_subgroup:
-  "subgroup H G" .
+  "subgroup H G" by fact
 
 declare (in subgroup) group.intro [intro]
 
@@ -694,7 +694,7 @@
 
 lemma (in group) subgroup_imp_group:
   "subgroup H G ==> group (G(| carrier := H |))"
-  by (rule subgroup.subgroup_is_group)
+  by (erule subgroup.subgroup_is_group) (rule `group G`)
 
 lemma (in group) is_monoid [intro, simp]:
   "monoid G"