increase font size in symbol index

[awodey]

against my own prior opinion, I think the font size in the symbol index should be increased to the match the main text, rather than the index. The reason is that symbols often involve (possibly iterated) sub- and superscripts, which get too small to read comfortably (at least for old eyes ...).

[cangiuli]

I tried it out; it causes a bunch of the descriptions to wrap onto a second line, but otherwise looks fine, and doesn't actually change the page count of hott-ustrade. Do we still want this?