changeset 26204 | da9778392d8c |
parent 23464 | bc2563c37b1a |
child 27611 | 2c01c0bdb385 |
--- 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