# HG changeset patch
# User ballarin
# Date 1229523633 -3600
# Node ID fa3fb943a0910d0f501bd15d15191cb765e8e761
# Parent  f7ffe90879e26988d42a2717a831ef4702106040
Attributes not applied in foundational version of fact.

diff -r f7ffe90879e2 -r fa3fb943a091 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)