src/HOL/Algebra/Group.thy
changeset 26199 04817a8802f2
parent 23350 50c5b0912a0c
child 26805 27941d7d9a11
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Mar 05 14:34:39 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:24:03 2008 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4    assumes Units: "carrier G <= Units G"
     1.5  
     1.6  
     1.7 -lemma (in group) is_group: "group G" by fact
     1.8 +lemma (in group) is_group: "group G" by (rule group_axioms)
     1.9  
    1.10  theorem groupI:
    1.11    fixes G (structure)
    1.12 @@ -383,7 +383,7 @@
    1.13      and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
    1.14  
    1.15  lemma (in subgroup) is_subgroup:
    1.16 -  "subgroup H G" by fact
    1.17 +  "subgroup H G" by (rule subgroup_axioms)
    1.18  
    1.19  declare (in subgroup) group.intro [intro]
    1.20  
    1.21 @@ -694,7 +694,7 @@
    1.22  
    1.23  lemma (in group) subgroup_imp_group:
    1.24    "subgroup H G ==> group (G(| carrier := H |))"
    1.25 -  by (erule subgroup.subgroup_is_group) (rule `group G`)
    1.26 +  by (erule subgroup.subgroup_is_group) (rule group_axioms)
    1.27  
    1.28  lemma (in group) is_monoid [intro, simp]:
    1.29    "monoid G"