Make sure all HTML pages are interpreted as utf-8 encoded

E.g. computeLib.CBV_CONV didn't display properly before this commit

Also use the "html5 doctype" in affected files

Definition HTML documentation hack

Adds DefinitionDoc signature to make new_definition etc. visible in the HTML
documentation. Hack inspired by HolKernelDoc.

This is a workaround for issue #238.

Use file extension “txt” for compiled built-in help files.

The previous extension “adoc” is used for ASCIIdoc markup language. “txt” is
more appropriate because this is plain text.

Have another go at getting HTML documentation working for HolKernel.

Address problem mentioned in commit 06487da.

A sig file line

val f: ty

should now link to documentation for "f".

Also fixed things so that the entries in Final{Type,Term,Thm}.sig link to the appropriate documentation.

There's still no HTML documentation for entries in HolKernel because it doesn't have a sig file. Don't know how to get around that.

Purge on broken links within the (HTML) documentation. This mostly involves
deleting SEEALSO entries (where documentation doesn't exist) but also fixing a
few links.

Also fixed the anchor links in TheoryIndex.html and idIndex.html. In both
cases there aren't any entries starting with the letter "Y".

Modify the HTML generation code to emit valid HTML 4.01 strict.

While idly waiting for a big check-in to happen to the web-pages
directory, I decided to edit this HTML generation code to make its
HTML elements use lower-case (i.e., <a href="foo">..</a>, rather than
<A HREF="foo">..</A>).

Make this directory build Moscow ML versions of the help executables,
promoting Scott's PolyML version of Database to be the primary
version. In general, take the attitude that PolyML sources here can
be primary, and that the Moscow ML stuff can be made to work with
appropriate use of My* structures, and Holmakefile magic.
When this is confirmed to work (really just need to test makebase),
I will remove help/src entirely.

Got the help build system working on PolyML.

Start working on porting the doc building system to SML (i.e., not Moscow ML)
to get it working with Poly ML.