Typo fixes and minor (HTML-level) reformatting.