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