src/HOL/Algebra/RingHom.thy
changeset 29240 bb81c3709fb6
parent 29237 e90d9d51106b
child 29246 3593802c9cf1
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:41 2008 +0100
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:56 2008 +0100
     1.3 @@ -10,7 +10,8 @@
     1.4  section {* Homomorphisms of Non-Commutative Rings *}
     1.5  
     1.6  text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
     1.7 -locale ring_hom_ring = R: ring R + S: ring S +
     1.8 +locale ring_hom_ring = R: ring R + S: ring S
     1.9 +    for R (structure) and S (structure) +
    1.10    fixes h
    1.11    assumes homh: "h \<in> ring_hom R S"
    1.12    notes hom_mult [simp] = ring_hom_mult [OF homh]