% and a page number in the margin. We use \inothermargin, since it is slightly
% bigger.
% This automatically prefixes the reference name with def:
% and a page number in the margin. We use \inothermargin, since it is slightly
% bigger.
% This automatically prefixes the reference name with def: