Fix lambda/typing example given 'perm_type' changes.

Extract a usable half-way point from nominal_datatype branch.

This replaces the is_perm predicate with a type embodying that predicate.
It doesn't include the subsequent work on allowing multiple 'atom' types.

Get lambda/typing directory to build again.

Had to deal with termScript stealing the \rightarrow syntax (I made
that theft local to termScript); and with tight equality.

Minor tidy-ups to sttScript; no long need to Unicode trace, for example.

Tidy up typing proofs (more Unicode!), and fix a proof broken by LIST_EQ_SIMP.

Hrumph. Even though the parser knows nothing of "B", CHOOSE_THEN or
some other deep dark internal is still deciding to prime B when it
appears in an assumed theorem like "?B. ..." This breaks the
hastype_lam_inv proof. I fix it for the moment to use entirely
different names, but am going to look into the other behaviour too.
Compare:
STRIP_TAC ([], ``(?B. P B) ==> P A``)
and
STRIP_TAC ([], ``!B. P B ==> P A``)
The first primes B, the second doesn't. (In a standard hol install,
replace B with C and you should see something similar because of C's
presence as a constant in combinTheory.)

Explicitly hide the "B" combinator that I just introduced in
chap2Theory so that I can continue to use it as a free variable name
in my simple typing theory.
(That's the problem with those dang combinators.)

Fiddle and prettify basic presentation of beta-reduction. Using
syntactic patterns, I can now have ``compat_closure beta M N`` (the
"compatible closure of the beta-relation) appear as ``M -b-> N``.
Also use syntactic patterns to get rid of constants reduction and
conversion. Finally, provide Unicode versions of the various arrow
symbols so that with the Unicode flag on, the above will come out as
M -β-> N
Even in just ASCII, I think the theorems look a deal prettier.

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

Fixes for these examples, and an updated MANIFEST/README in
other-models. The other-models directory had become particularly
stale. I obviously need to check that it works more often. (Main
problem: change to behaviour of Q.INST.)

Continue to make the typing sub-directory of the lambda-calculus
example as Unicodified as possible, as a general test-case of what the
technology allows. (Now I can have Unicode universals as binders
in Hol_reln calls, and Unicode strings as bound variables.)

Unicode prettification.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

Make the typing relation look even prettier by using Unicode
characters corresponding to LaTeX's \vdash and \lhd in the concrete
syntax. (The ASCII version is still around and can be used for input
too.)

Make this theory even more Unicodified.

Refactor simple type theory development by moving theory of contexts
as association lists on strings to a separate theory.

Make a new directory containing some work on simple typing for the
lambda calculus.