src/FOL/ex/NewLocaleTest.thy

--- a/src/FOL/ex/NewLocaleTest.thy	Tue Dec 16 20:18:46 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 17 15:20:33 2008 +0100
@@ -164,6 +164,9 @@
   assumes semi_homh: "semi_hom(prod, sum, h)"
   notes semi_hom_mult = semi_hom_mult [OF semi_homh]
 
+thm semi_hom_loc.semi_hom_mult
+(* unspecified, attribute not applied in backgroud theory !!! *)
+
 lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
   by (rule semi_hom_mult)