underscore in BibTeX keys means trouble: do not use it

double 'the' removed

More tidying in the Tutorial's Chapter 3.

Closes #35.

Some initial tidy-up work on logic.tex in Manual/Tutorial.

Focus on normalising TeX sources so each sentence gets a line to
itself. Also make some other minor changes along the way.

This is progress with #35

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

Remove some trailing whitespace.

Make point in Tutorial that structures may need to be opened.

In response to a comment from a user.

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.

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.

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

Fix for bug #602657.

A variety of updates in the light of Kananaskis changes.

Typo corrections. Typos spotted by Anthony Fox.

Fixed minor typo in text of logic; updated Makefile to produce postscript
as well as pdf output.

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

Various changes suggested by Konrad.

Examples tidied up so that terms are quoted as being pretty-printed back
to the user with double back-quotes, which they are, now that I've fixed
that problem in the source.

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.

Revised a bit more. Have decided that Peano axiomatization should be
replaced with example over binary trees, possibly even involving some
simple proof. The script can be turned into a compiled theory as well.

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.

Tutorial added to repository; builds under LaTeX2e.