add filter operation to HOLSet

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

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!

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