* You must have Moscow ML 2.00 fully installed to build HOL or to run
  the self-installing program.  This includes having the appropriate
  environment variables set (you need both MOSMLLIB, and a new entry
  in PATH).

* If running the ``HOL`` version of hol98 (hol.unquote), you will not
  be able to exit from the interactive program with quit().  Instead,
  you will have to type the eof combination Ctl-Z <RET>.

* The very last stage of the installation process is to run a program
  called win-config.  If this doesn't work for some reason (maybe
  because you haven't set up the environment variables that Moscow ML
  depends on properly), then you can run it yourself to complete the
  process.  Open up an MS-DOS shell, cd to the tools directory within
  the HOL source, and type, for example,
    win-config "c:\program files\Hol"
  where the argument to the command is the path of where HOL was
  installed.