src/HOL/Algebra/AbelCoset.thy
changeset 28823 dcbef866c9e2
parent 27717 21bbd410ba04
child 29237 e90d9d51106b
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4    by (rule a_normal)
     1.5  
     1.6    show "abelian_subgroup H G"
     1.7 -  by (unfold_locales, simp add: a_comm)
     1.8 +  proof qed (simp add: a_comm)
     1.9  qed
    1.10  
    1.11  lemma abelian_subgroupI2:
    1.12 @@ -549,7 +549,7 @@
    1.13  
    1.14  lemma (in abelian_group_hom) is_abelian_group_hom:
    1.15    "abelian_group_hom G H h"
    1.16 -by (unfold_locales)
    1.17 +  ..
    1.18  
    1.19  lemma (in abelian_group_hom) hom_add [simp]:
    1.20    "[| x : carrier G; y : carrier G |]