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.

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.

Fix barendregt/chap2Script.sml so that set_MLname is no longer required.

Also fix annoying choice of names while I'm at it.

Tidy up some proofs by using Once and the new Simp* modifiers to the
simplifier (replacing things like CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV ...)))

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Changes so that the weakened rewriting of lambda-terms now happens
with respect to beta-equality (==), rather than beta-reduction
(-b->*). This gives us access to more rewrites. In particular, we
get things like
church (SUC n) @@ z @@ f == f @@ (church n @@ z @@ f)
which is a nice recursive characterisation of what church numerals do,
and saves us from having to do too many ghastly things with FUNPOW.
With the above equation, neither side reduces to the other (they have
a common reduct of course), and so it wasn't a usable rewrite when
using -b->*.

In addition, to the above, I set up a natrec combinator, which would
get typed
: 'a -> (num -> 'a -> 'a) -> num -> 'a
if we were in a typed world. This combinator gets access to the value
of the recursive argument, making predecessor easier to define.

Also, give an equation like the one above for church for the cDB
function.

Many proofs are shorter. Some are slower, but the shortness of
expression won me over.

Add some rewrites about freshness (not being in the free variables of
a term) that work better with the simplifier. This breaks a couple of
proofs later on in chap2 and chap3 theories, that are easily fixed.

More useful facts about Omega, including the fact that if you can
reach it, you have no beta-normal-form.

More facts about normal order reduction paths, including the fact that
the self-looping Omega term has an infinite one, and thus, by another
theorem just proved, has no beta-normal-form.

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.

Start to move stuff relating to head-reduction into a separate
theory. There's still a pile of stuff, mainly expressed in terms of
reduction paths, in standardisationTheory that could probably be moved
or re-expressed. In particular, there is a head_reduce1 constant
there that is actually the same as -h-> from head_reductionTheory.

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.

Improve the statement of strong_ccbeta_gen_ind, save it to disk, and
alter the one proof that relies on it.

Fix for the lambda-calculus examples in light of RTC_REFL being exported
from relationTheory.

More laggards.

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