Footnote 1: This policy was adopted before @undef had been invented; it might be better to warn about duplicates and require explicit undefinition before redefining.