Remove TABs from src

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

add filter operation to HOLSet

A filter operation was useful for sets. This commits adds it to
Redblackset and thereby indirectly to HOLSet.

Fix bug in Redblackset.isSubset (empty sets were only subsets of empty sets)

This came up while investigating github issue #113

Function fromList added.

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!

In preparation for making the standard kernel build under Poly/ML, removed the dependency of src/0/Term.sml on the Moscow ML library Polyhash, replacing this with RedBlackMap.

The building of HOL appears to be faster with RedBlackMap.

Also revised RedBlackMap.sml, RedBlackSet.sml, and HolKernel.sml to eliminate some annoying warning messages.

Special-case optimisation for RB set union: if one set is sufficiently smaller than the other then just insert its elements into the bigger set. Based on ancient correspondence with Ken Friis Larsen.

Fix the bug that was allowing the add operation to leave the tree unchanged.

Stuff that people tell me will appear in the next MoscowML release.