src/HOL/Algebra/RingHom.thy
changeset 21502 7f3ea2b3bab6
parent 20318 0e0ea63fe768
child 23350 50c5b0912a0c
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Nov 23 20:33:42 2006 +0100
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Nov 23 20:34:21 2006 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  section {* Homomorphisms of Non-Commutative Rings *}
     1.6  
     1.7 -text {* Lifting existing lemmas in a ring\_hom\_ring locale *}
     1.8 +text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
     1.9  locale ring_hom_ring = ring R + ring S + var h +
    1.10    assumes homh: "h \<in> ring_hom R S"
    1.11    notes hom_mult [simp] = ring_hom_mult [OF homh]