work on temporal_deep example

Following some work by Chun Tian, this commit makes the temporal_deep
example compile again. This example got severe bit-rot unluckily. There
is still more work to do:

- the libraries have not been tested yet
- the theories contaimn now many constants and lemmata now present in
standard libraries
- the proofs are ugly using strange constructs which are hard to
maintain (I hope I learned something about HOL within the last 10 years
since I created this example)

So, this commit is just a first step and more cleanup work will follow.

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!

Some deep embeddings of temporal logics and some related tools. Especially there are translations between PSL and LTL and between LTL and omega-automata. Additionally, there is an interface to SMV