src/HOL/Algebra/AbelCoset.thy
changeset 26203 9625f3579b48
parent 23463 9953ff53cc64
child 26310 f8a7fac36e13
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:33:59 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:42:21 2008 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4  
     1.5  lemma (in additive_subgroup) is_additive_subgroup:
     1.6    shows "additive_subgroup H G"
     1.7 -by fact
     1.8 +by (rule additive_subgroup_axioms)
     1.9  
    1.10  lemma additive_subgroupI:
    1.11    includes struct G
    1.12 @@ -225,7 +225,7 @@
    1.13  
    1.14  lemma (in abelian_subgroup) is_abelian_subgroup:
    1.15    shows "abelian_subgroup H G"
    1.16 -by fact
    1.17 +by (rule abelian_subgroup_axioms)
    1.18  
    1.19  lemma abelian_subgroupI:
    1.20    assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"