author | wenzelm |
Wed, 05 Mar 2008 21:48:15 +0100 | |
changeset 26204 | da9778392d8c |
parent 26203 | 9625f3579b48 |
child 26205 | 499f08293680 |
--- a/src/HOL/Algebra/RingHom.thy Wed Mar 05 21:42:21 2008 +0100 +++ b/src/HOL/Algebra/RingHom.thy Wed Mar 05 21:48:15 2008 +0100 @@ -33,7 +33,7 @@ lemma (in ring_hom_ring) is_ring_hom_ring: includes struct R + struct S shows "ring_hom_ring R S h" -by fact +by (rule ring_hom_ring_axioms) lemma ring_hom_ringI: includes ring R + ring S