theory AB
  imports A B
begin
