author | wenzelm |
Thu, 11 May 2023 10:46:52 +0200 | |
changeset 78031 | a526f69145ec |
parent 78030 | ec9840c673c3 |
child 78032 | 73c77db63594 |
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed May 10 23:28:15 2023 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu May 11 10:46:52 2023 +0200 @@ -234,7 +234,7 @@ notes semi_hom_mult = semi_hom_mult [OF semi_homh] thm semi_hom_loc.semi_hom_mult -(* unspecified, attribute not applied in backgroud theory !!! *) +(* unspecified, attribute not applied in background theory !!! *) lemma (in semi_hom_loc) \<open>h(prod(x, y)) = sum(h(x), h(y))\<close> by (rule semi_hom_mult)