Class.thy revision 255a89789d3d5b19f6a8c96bf6c260a96158ef6d
theory Class
imports HOL Nat
begin
class parent =
fixes p1 :: "'a => 'a => 'a"
assumes a1: "p1 a b = p1 b a"
class child = parent +
fixes p2 :: "'a"
and p3 :: "'a"
and p4 p5 :: "'a"
assumes a2: "p1 p2 x = x"
end