src/HOL/Algebra/RingHom.thy
changeset 30729 461ee3e49ad3
parent 29246 3593802c9cf1
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -61,8 +61,8 @@
     1.4    assumes h: "h \<in> ring_hom R S"
     1.5    shows "ring_hom_ring R S h"
     1.6  proof -
     1.7 -  interpret R!: ring R by fact
     1.8 -  interpret S!: ring S by fact
     1.9 +  interpret R: ring R by fact
    1.10 +  interpret S: ring S by fact
    1.11    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    1.12      apply (rule R.is_ring)
    1.13      apply (rule S.is_ring)
    1.14 @@ -78,8 +78,8 @@
    1.15    shows "ring_hom_ring R S h"
    1.16  proof -
    1.17    interpret abelian_group_hom R S h by fact
    1.18 -  interpret R!: ring R by fact
    1.19 -  interpret S!: ring S by fact
    1.20 +  interpret R: ring R by fact
    1.21 +  interpret S: ring S by fact
    1.22    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    1.23      apply (insert group_hom.homh[OF a_group_hom])
    1.24      apply (unfold hom_def ring_hom_def, simp)
    1.25 @@ -94,8 +94,8 @@
    1.26    shows "ring_hom_cring R S h"
    1.27  proof -
    1.28    interpret ring_hom_ring R S h by fact
    1.29 -  interpret R!: cring R by fact
    1.30 -  interpret S!: cring S by fact
    1.31 +  interpret R: cring R by fact
    1.32 +  interpret S: cring S by fact
    1.33    show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    1.34      (rule R.is_cring, rule S.is_cring, rule homh)
    1.35  qed