theory Locale
imports HOL
begin
locale semi =
fixes prod :: "['a, 'a] => 'a" (infixl "*" 70)
and test
assumes assoc: "(x * y) * z = x * (y * z)"
locale comm_semi = semi +
assumes comm: "x * y = y * x"
and test: "False=x & ~x"
and test1: "y=y"
and test2: "x=x"
locale parent
locale parent1
locale child = parent + parent1
end