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
```