Most of the time, the <dt> tag is used when providing
documentation for a symbol; enclose symbols in <code> tags to
style them appropriately.