Changed hol-mode.src and src/parse/PPBackEnd.sml so that type variables are displayed in purple.

"Everybody's cute... Everybody's cute, even me. But in purple, I'm STUNNING!"
(Centauri Ambassador Londo Molari, Babylon 5, The Parliament of Dreams)

guess_word_lengths --> inst_word_lengths.

Minor update on building the HolBdd code, and remove the -expk flag
from the build instructions for Poly/ML.

Fix a typo in the description of rewriting with arbitrary pre-orders.

HolSmtLib mentioned.

Add note to release notes saying that machine-code example needs Poly.

Slightly reformat Peter's HTML; and add a paragraph about the
machine-code example.

This adds to the Kananaskis-5 release documentation a description of HOL-Omega as a new version of HOL4.

Slightly reword a sentence in the release notes that confused me when
I came to re-read it.

Right a brief introductory paragraph to the release notes, with space
also perhaps for something about Peter's HOL-Omega system.

Mention the STE example in the release notes.

Update release notes to say that UTF-8 proving works fine on Windows with recent versions of Emacs.

Add mention of Anthony's theory about Patricia trees. (Feel free to
add anything you like to flesh this out Anthony.)

Add mention of trick to overcome backwards incompatibility of handling
of unary minus for words, and also mention new "rewrite with pre-order"
functionality.

A bit more on how to use prefix and infix operators simultaneously.
In particular, you can't use set_fixity to set up the second one.

Implement unary minus (the old ~ still also works). Selftest level 2
passes. Changes in the "words world" were replacing $- with -. In
the two quotient changes, I made sure that the infix operator
that used the - character was part of the grammar before it was
parsed. This is necessary because - is now a non-aggregating
character, mainly so that ``--p`` parses as three tokens, not two. Of
course, if you added -- to your grammar, then it would go back to
parsing as two.

Modify release notes to reflect improvement in lexing, and make use of
new facilities in simple type theory example.

Updated release notes to mention syntactic patterns.

Some more fixes, including to a couple of examples that grep turned up
as using Infixr 450.

Mention my changes to add_user_printer in the incompatibilities
section of the release notes.

Update release notes to mention new limit function. (Also validate it
with online tool at w3.org, prompting some minor fixes.)

Get the new version of parse_in_context to work properly (two stupid
errors fixed), and also document the potential incompatibility in the
release notes. (Also remove talk of Define using conjunction and
disjunction congruence rules.)

Create a "new feature" entry for Unicode support in the release notes.

Realised that the release notes should say that version 5.2 of Poly/ML
is required.

Document existence of polyml port in the release notes, and also in
the process of documenting recursive Holmake and the --no_prereqs
option, add a feature to Holmake allowing NO_PREREQS to be an OPTION
as well. Document the latter in the Description (also add some \index
entries there).

(We are going to have to merge the Holmake implementations if at all
possible; having to update two versions is a pain.)

Move pred_set to be earlier in the build sequence, making it an
ancestor of listTheory, and available in bossLib. The various
LIST_TO_SET and SET_TO_LIST theorems are now available in listTheory.
Also introduce the set abbreviation for LIST_TO_SET that I've found
very useful. Documented in release notes as an incompatibility.
Incidentally reckon containerTheory might be something we could do
away with entirely.

Added a bug-fix report for a build-error that existed on Windows.

Fixes to release notes. Added Anthony's check-in message about new
wordsLib facilities, replaced "sat-solver" with "SAT solver" and made
the HTML validate.

I've run through our check-in messages from 2007 and made the release
notes for K-5 look as if we've actually been doing stuff. I'm itching
to release sooner rather than later, so please check that I've
correctly described what you've done. I've ignored all examples
except my silly little DPLL thing, but if your example has changed
and you want to tell the world about it, please put the news into the
examples section (which you can rename to "Examples Updates" or
something).

Give the Windows filenames backslashes consistently.

Update release notes to describe what we've done to muddy and friends.

Remove one of the last remaining vestiges of "hol98"; in the Emacs mode.

Start to write release notes. I've no idea what else needs going in
here.