alltt is now part of a standard LaTeX distribution
extra space in verbatim text removed
whitespace cleanup
extra space in type description removed
HO_MATCH_MP_TAC: new documentation and fix of failure report
random fixes in reference manuals:
 - single instead of double semicolons (ML prompts);
 - double backticks instead of single quotes (terms).

These are probably a legacy of old HOL implementations.
Merge pull request #207 from ptroja/master

HO_MATCH_MP_TAC documentation (and other minor fixes)