src/HOL/Algebra/AbelCoset.thy
changeset 30729 461ee3e49ad3
parent 29237 e90d9d51106b
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -540,8 +540,8 @@
     1.4                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
     1.5    shows "abelian_group_hom G H h"
     1.6  proof -
     1.7 -  interpret G!: abelian_group G by fact
     1.8 -  interpret H!: abelian_group H by fact
     1.9 +  interpret G: abelian_group G by fact
    1.10 +  interpret H: abelian_group H by fact
    1.11    show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    1.12      apply fact
    1.13      apply fact
    1.14 @@ -692,7 +692,7 @@
    1.15    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    1.16    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
    1.17  proof -
    1.18 -  interpret G!: ring G by fact
    1.19 +  interpret G: ring G by fact
    1.20    from carr
    1.21    have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
    1.22    with carr