1
theory Semigroup = Main:;
2
3
consts
4
times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 70);
5
axclass
6
semigroup < "term"
7
assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
8
9
end;