Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

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.

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.

Rework lambda-term recursion principle proof once more.

It's simpler and more polished, mostly following the IJCAR'06 paper by
Urban and Berghofer, though slightly simpler even than that. I
believe I have one more useful change in me for this development, and
then I'll attempt to do the whole thing again, generically in
genericTerms.

The change to term_posnScript comes about because it relied slightly
too much on the exact form of the principle. (Previously tm_recursion
was just recursion and not iteration; putting iteration in from the
outset seems harmless.)

Implement a new (automatic) simplification for terms like {(x,y)|F}.

Such terms rewrite to {}, but with the underlying paired abstractions
getting in the way, it's impossible to get a normal rewrite to do the
right thing. The implemented conversion also tries to handle the
situation where the predicate is T, but this isn't sure to rewrite to
UNIV because pattern-forms may preclude it. For example,
{ x + 1 | T }
with x a natural, is not the universal set.

The simpset fragment has name GSPEC_SIMP if you need to remove it.
The distribution builds at selftest level 1. Selftest level 2 will be
tested overnight.

Proof fixes given general incorporation of LIST_EQ_SIMP_ss.

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