use LaTeX quotes ``...'' instead of "..."

Changes to the Description. Still highly in flux, but I wanted to
get the changes into CVS.

Many updates. Three main, parallel activities:
* removal of cruft
* descriptions of "new" theories (llist, path, finite maps, posets)
* description of "new" technology (simpLib, meson, metis, cooper's alg)
Not that all of this is done. In fact some of it hasn't even been started
yet.

Some minor corrections.

Minor updates that I spotted in passing.

Changed Taupo-3 to Taupo-4 on title page, and reworked a reference to
Taupo-1 in the description of the parser to just be Taupo releases and
beyond or somesuch.

Modified to use Charter, a Postscript font which produces much cleaner
.pdf output. A PDF version of the Description is also produced in the
Makefile.

Added some parser tricks.

Updated the description of Hol_datatype and record types. Did a global
replace of HOL98 and Hol98 with \holn{}, which is now defined in
commands.tex. The choice there of \textsf{hol98} can of course be
changed, but at least we will have a consistent choice now.

Added new chapter on syntax stolen from hol98 manual. It duplicates some
existing material and needs extending.