theory B imports Pure
begin

end