src/HOL/Algebra/RingHom.thy
changeset 44655 fe0365331566
parent 35849 b5522b51cb1e
child 61169 4de9ff3ea29a
--- a/src/HOL/Algebra/RingHom.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -17,7 +17,7 @@
     and hom_one [simp] = ring_hom_one [OF homh]
 
 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
-  proof qed (rule homh)
+  by default (rule homh)
 
 sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
 apply (rule abelian_group_homI)