src/HOL/Algebra/RingHom.thy
changeset 23463 9953ff53cc64
parent 23350 50c5b0912a0c
child 23464 bc2563c37b1a
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:50 2007 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:53 2007 +0200
     1.3 @@ -46,7 +46,10 @@
     1.4    shows "ring_hom_ring R S h"
     1.5  apply unfold_locales
     1.6  apply (unfold ring_hom_def, safe)
     1.7 -   apply (simp add: hom_closed Pi_def, assumption+)
     1.8 +   apply (simp add: hom_closed Pi_def)
     1.9 +  apply (erule (1) compatible_mult)
    1.10 + apply (erule (1) compatible_add)
    1.11 +apply (rule compatible_one)
    1.12  done
    1.13  
    1.14  lemma ring_hom_ringI2:
    1.15 @@ -67,13 +70,16 @@
    1.16  apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
    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, assumption+)
    1.20 +apply safe
    1.21 +apply (erule (1) compatible_mult)
    1.22 +apply (rule compatible_one)
    1.23  done
    1.24  
    1.25  lemma ring_hom_cringI:
    1.26    includes ring_hom_ring R S h + cring R + cring S
    1.27    shows "ring_hom_cring R S h"
    1.28 -by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh)
    1.29 +  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    1.30 +    (rule R.is_cring, rule S.is_cring, rule homh)
    1.31  
    1.32  
    1.33  subsection {* The kernel of a ring homomorphism *}