explicit referencing of background facts;
authorwenzelm
Wed Mar 05 21:48:15 2008 +0100 (2008-03-05)
changeset 26204da9778392d8c
parent 26203 9625f3579b48
child 26205 499f08293680
explicit referencing of background facts;
src/HOL/Algebra/RingHom.thy
     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