Provide \bq macro for teletype backquote (`) character

Adjust release name in Manuals

Make early Description text more Unicode aware

Remove -- from doc-files.

Thanks to Andreas for pointing this out.

Use ##thm command to get nice theorems printed in Description

Still many more of these to work through; for the moment only those in
the section on finite_mapTheory are done.

More hacking at Description's Tactics chapter

Next release will be Kananaskis-11

This commit starts release preparation branch.

Set arbitrary traces while LaTeX munging.

Closes #141. That issue calls for a slightly different interface to
get much the same effect. This approach has the advantage that it
keeps the effect of the trace changing localised.

Change Kananaskis-9 into Kananaskis-10 in the relevant places.

Make \ie, \eg and \etc LaTeX macros expand to text in italic shape.

DESCRIPTION: fixed punctuation, style and typography of 'etc.'

Typography: problematic macros marked with FIXME notes.

Updated version number in manuals, banners etc.

Change HOL macro in manuals to be \textsc{Hol}.

The old macro was to {{\small HOL}} which meant that uses of \HOL in
things like section titles looked awful. The new form looks better in
that context but may well not be the final word.

Update version numbers now that K7 is out.

Bump version numbers - next release to be 'Kananaskis-7'.

From now on we're in the Brave New World of Kananaskis 6.

Add some documentation of the "syntactic patterns" feature.

Write a brief section on Unicode features in the parser.

Much hacking about with the Description manual. Section headings more
consistent, index tidied, some prose written about tokens in the brave
new world of Unicode aware parsing.

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.

Bump our release number to 5, for the next release. Will probably remove
the original uses in help/src and just make these reference the Globals
module.

New command for the fourth manual.

Another place where version numbers get bumped for the next release.

Minor index hacks, as well as adjusting the \holquote macro to print out
a more accurate reflection of what the user sees (\tt backquotes, in other
words).

Add new \holtxt command. Intention is to ultimately replace all those ugly
\verb+..+ and {\small\verb+...+} with calls to \holtxt and \ml, depending
on the nature of the contents. Currently, both \holtxt and \ml look the
same, but distinguishing is still worthwhile I think. To get backslashes
in \holtxt or \ml, use \bs.

Added a macro or two.

Some useful commands, including one for generating a texttt backslash,
that's \bs.

Update the numbers corresponding to our version number.

Update holversion macros for new release and remove unused VERSION macro.

Modified Holmake to support a -i (or --interactive) command-line flag.
(This is feature request #611879.) Modified documentation to reflect this
and slightly updated some other things in the Description that caught my
eye.

Remove annoying messages about \sl not being allowed in math-mode by
replacing occurrences with \textsl. Also remove unused files hol98.dot
and hol98.pic.

Most important hol98 purging action.

Changed the session environment so that they can be \label-ed, and then
later \ref-ed.

Updated macro for release name and version number.

Updated version number to 5.

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.

\holn macro now defined in commands.tex.

Removed the \see command, which is defined by the makeidx package.

Useful parts of the hol88 directory; copied across for hol98 and some
slightly updated.