src/HOL/Algebra/RingHom.thy
changeset 26204 da9778392d8c
parent 23464 bc2563c37b1a
child 27611 2c01c0bdb385
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Wed Mar 05 21:42:21 2008 +0100
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Wed Mar 05 21:48:15 2008 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  lemma (in ring_hom_ring) is_ring_hom_ring:
     1.5    includes struct R + struct S
     1.6    shows "ring_hom_ring R S h"
     1.7 -by fact
     1.8 +by (rule ring_hom_ring_axioms)
     1.9  
    1.10  lemma ring_hom_ringI:
    1.11    includes ring R + ring S