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