WIP: perm_type wasn't building; now it's closer to building.

I probably mangled my attempt to extract the 'good stuff' from the old
nominal_datatype branch. I have cleaned things up slightly by hiding
the 'raw' lswapstr constant. Now the string "lswapstr" maps to a term
that is a permutation action, making all the permutation rewrites
apply for lswapstr automatically.

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.

Revised Barendregt Chapter 11.1 theory

Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.

Rework lambda-theory scripts to use new varying parameter recursion theorem.

Also make work for myself by having some of the script files use
'tight' equality. Later files get switched back to loose (prec = 100)
equality, because it was all getting to be too much work.

Fully support weaker relations than equality that aren't also
constants. Start to implement a reduction engine for beta-reduction
in the lambda-calculus. Still some wrinkles to work out.

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.

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.)

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.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Completely reorganise these files into some sensible directories.
Also, add a file demonstrating that the McKinna-Pollack two-sorted raw
syntax does indeed behave properly (links appropriately to beta over
quotiented terms).