
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -34,7 +34,7 @@
 lemma (in ring_hom_ring) is_ring_hom_ring:
   includes struct R + struct S
   shows "ring_hom_ring R S h"
-by -
+by fact
 
 lemma ring_hom_ringI:
   includes ring R + ring S
@@ -51,9 +51,13 @@
 
 lemma ring_hom_ringI2:
   includes ring R + ring S
-  assumes "h \<in> ring_hom R S"
+  assumes h: "h \<in> ring_hom R S"
   shows "ring_hom_ring R S h"
-by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (rule R.is_ring)
+apply (rule S.is_ring)
+apply (rule h)
+done
 
 lemma ring_hom_ringI3:
   includes abelian_group_hom R S + ring R + ring S 




