Fix examples/lambda/other-models for tight equality

Reconcile store_thms with diverging names in db and val binding

Remove eqtype declaration for term type

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Fix more lambda-calculus theories for pat_assum rename

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!

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