src/HOL/Algebra/RingHom.thy
changeset 23464 bc2563c37b1a
parent 23463 9953ff53cc64
child 26204 da9778392d8c
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:53 2007 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Jun 21 20:07:26 2007 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  imports Ideal
     1.5  begin
     1.6  
     1.7 -
     1.8  section {* Homomorphisms of Non-Commutative Rings *}
     1.9  
    1.10  text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
    1.11 @@ -67,7 +66,7 @@
    1.12    assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.13        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.14    shows "ring_hom_ring R S h"
    1.15 -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
    1.16 +apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    1.17  apply (insert group_hom.homh[OF a_group_hom])
    1.18  apply (unfold hom_def ring_hom_def, simp)
    1.19  apply safe