Make some early HOL libraries more robust to changed grammar ctxts

This is mostly unnecessary given that these libraries are all bundled
into the default hol.state heap and are thus loaded once in a known
context. However, having defined instances of the parser, and not
using quotation based tactics (e.g., Cases_on) is still good practice.

Remove TABs from src

Will also make selftest to check that they aren't introduced

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!

Getting rid of some pattern-matching complaints,
as Anthony suggested.

Fixed Lockwood Morris' problem with UNION_CONV.

Fixed bug in set conversions: the constant IN is no longer defined in
pred_setTheory, but in boolTheory, for some reason.

Also added rudimentary syntax support for sets.

Removed IN as a constant from pred_set theory now that it's in bool.
Somewhat to my surprise, things built anyway, but it was distracting
seeing the messages complaining about the ambigous grammars and the
overloading resolution. (I shouldn't be surprised of course, this is
the whole point of all the Kananaskis work!)

Minor changes.

Now builds in Kan.0.

Kananaskis compatibility.

Initial revision