| changeset 28823 | dcbef866c9e2 |
| parent 27717 | 21bbd410ba04 |
| child 29237 | e90d9d51106b |
--- a/src/HOL/Algebra/RingHom.thy Mon Nov 17 17:00:27 2008 +0100 +++ b/src/HOL/Algebra/RingHom.thy Mon Nov 17 17:00:55 2008 +0100 @@ -17,7 +17,7 @@ and hom_one [simp] = ring_hom_one [OF homh] interpretation ring_hom_cring \<subseteq> ring_hom_ring - by (unfold_locales, rule homh) + proof qed (rule homh) interpretation ring_hom_ring \<subseteq> abelian_group_hom R S apply (rule abelian_group_homI)