src/HOL/Algebra/RingHom.thy
changeset 61169 4de9ff3ea29a
parent 44655 fe0365331566
child 61382 efac889fccbc
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:56:52 2015 +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 -  by default (rule homh)
     1.8 +  by standard (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)