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