Fix installation instructions in Tutorial's introduction

Again, preferring Poly/ML over Moscow ML, but mentioning need for
Cygwin or Linux sub-system if using Windows.

More minor Tutorial tweaks

Minor tweaks to intro and ML chapters of Tutorial

Remove docs saying --enable-shared must be used

Adjust installation instructions a little.

From comments in github issue #324:
* tell users not to use the --with-portable option when building Poly/ML
* make it clear that the system installs "in place", and that once build
has done its thing, the system can't be moved.

Closes #324

Update installation instructions to include need for --enable-shared

Update URL for Moscow ML.

Document requirement to have dynamic loading working for Poly/ML.

Fix LaTeX error in Tutorial.

Use the \HOL macro in manuals' section headers now it looks OK.

Renamed install.txt to INSTALL for the sake of uniformity.

Given that Poly/ML requires the experimental kernel, there's no point
in requiring the user to remember to type -expk when doing a build.
(Will merge this into K5; hopefully this will be the last change
there, except possibly to the Windows self-installer generation.)

Update our installation instructions, both in install.txt and in the
Tutorial. The latter needed to mention that only -expk works with
Poly/ML. I can't see this changing before the release.

Update the Tutorial for the forthcoming release:
* introduction now describes the Poly/ML option
* combinatory logic example uses syntactic pattern overloading to
avoid having to define specific constants for RTC (-->) and
RTC (-||->). This makes things a little shorter (which is all to
the good).

Now require users to do their configuration from the root HOL
directory (updating the documentation to reflect this). The reason is
to enable both
mosml < tools/smart-configure.sml
and
poly < tools/smart-configure.sml
The contents of tools/smart-configure.sml now figures out which
interpreter is being run (by relying on a known mosml bug), and then
runs the real configuration script for the given ML system.

This would be a lot simpler if mosml's default environment included
the CommandLine structure from the Basis Library.

Have "modernised" the manuals.

1. By default it now uses pdflatex. Postscript can still be generated
with "make ps".

* Authors should not use pstricks - it doesn't work with pdflatex.
* The commuting diagrams in the tutorial have been redone with
XP-pic -- with much less code.
* Other figures can be included with "\includegraphics", which is provided
by the graphicx package. Just make sure you upload EPS and PDF versions
of the diagrams.
* The Covers directory and old logos have been removed -- they weren't
maintainable. (Have tarted up the title.tex pages.)

2. The make files have been updated and cleaned up. There is
now "make clean" option in $HOLDIR/Manuals.

* As a side note, I noticed that a call to "make" in $HOLDIR/Manuals didn't
do anything on Mac OS X. I had to do "make -B".

3. Have eliminated font substitution errors.

* Don't include the charter.sty package - the font is now changed
in LaTeX/layout.sty. This avoids changing the \tt font, which
causes problems with \section{\texttt{stuff}}.
* Left and right braces in \tt font can be a problem. \{ and \} give
maths font, which is fine in places. \verb%{}% will work but
\verb can't be used in certain places (inside another command).
Have added \lb and \rb to LaTeX/commands.tex. These are just
\char'173 and \char'175 and can be used anywhere.

4. Have commented out the mucking about with page numbering.

* This means that if you do a goto page N (in Acrobat, Preview.app etc.)
then you go to page N of the main text. (Stops folks having to add
an offset to entries in the index.)

5. Have made things more compatible with amsmath.

* The environment "boxed" (LaTeX/commands.tex) has been renamed to "holboxed".
* Have changed "\over" to "\frac".
* amsmath is turned on in the Logic manual, mainly to get text subscripts
typesetting better.

6. Have removed a bunch of hbox (and other) warnings.

* Don't do "\begin{session}\begin{hol}\begin{verbatim}...", do
"\begin{session}\begin{verbatim}..." instead.
* Don't use "\begin{hol}\begin{verbatim}..." is item lists.
Instead just do "\begin{verbatim}".
* Have done some small text edits - hopefully these are okay.
* A few more warnings remain and there's not much that can be done
about underfull vboxes -- short of going with "\raggedbottom".

7. Have made Doc2TeX and reference.tex used fancyvrb, This means the
font size can be set to \small globally. Have also removed the
\samepage directive -- a few bad breaks are better than having
material bigger than the size of the page.

Microsoft keep releasing new versions of Windows, so I have added the
claim that HOL works on Vista as well as the others we supported. I
haven't actually tested this...

Some updates to HOL manuals. Main change is to SourceForge addresses,
but have also changed the Acknowledgements to reflect the fact that
the manual is no longer a "wide-ranging revision" and to also
list the names of important contributors. Some people may have been
left out; if so, please let me know.

Fixes for various infelicities.

Last change I want to make before releasing; change the MOSMLDIR value
to be the directory containing the mosml binaries, rather than being
the parent of this directory. This should make life easier on those
installations where the mosml install doesn't look like
mosml
+----- bin
+----- lib
(Some do not have bin and lib as siblings. The code using MOSMLDIR
never looks for anything except bin underneath it.)

Updates (to code and documentation) to better handle situation where
dynamic linking is not available. Now, the Systeml structure records
whether or not it is by storing a boolean in the variable DYNLIB.

Update to make our support for MacOS explicit.

Various updates, including removal of all references to hol.unquote.

Describe the new config-override behaviour.

I realised that time-zones meant I'd be first in on Monday, so I've made
the fix to configure.sml. I've also documented the new configuration
method in install.txt and the TUTORIAL.

Fix for bug #602199 (reported by Carl Witty).

Some changez purging hol98 from the documentation.

A variety of updates in the light of Kananaskis changes.

Fiddled slightly to better reflect the way things stand at the moment.

Typo corrections. Typos spotted by Anthony Fox.

Modified so that the hol version number information is accessed through
a macro, defined in the LaTeX/commands.tex file. This allows it to be
changed in one place instead of many.

Taupo-3's changed into Taupo-4's.

Reduced the number of explicit references to Taupo-1 in the text,
thereby reducing the degree to which the manual can be made obsolescent
by changing version numbers. Making sure that the examples are still
all correct is still not going to be easy.

Updated reference to older Taupo's to Taupo-3.

Minor changes to get slightly prettier html output.

Many more changes to make the Tutorial build better as a hevea translated
html document; the .dvi file produced is pretty much unaffected.

Suite of relatively minor changes. Most significant is addition of
final chapter that explains the contents of the examples directory.

Various changes suggested by Konrad.

Minor type-setting fixes.

Big revision; Euclid example from hol98 manual is now chapter 4.
Discussion of theories from chapter 3 has disappeared, but I think I'll
put an example of theory work into the end of the Euclid example.

Minor change in intro; completely converted ml.tex to be a brief
description of SML; started to convert logic.tex. Got as far as the
description of theories, which will probably need a fairly intensive
rewrite.

Complete revision of this to now instruct on how to install hol98 rather
than hol88. Probably needs to be a deal more explicit on how to cope with
possible errors.

Tutorial added to repository; builds under LaTeX2e.