Fix examples/temporal_deep given tight equality

temporal_deep example: ensure it works with both standard and experimental kernel

cleanup temporal_deep

- replace "ITERATE" with "FUNPOW"
- replace "POWER_SET" with "POW"
- replace "PRED_SET_FORALL" with "RES_FORALL"
- move "POS_START" to translationsLib and plan for later removal
- remove various lemmata and use lemmata from standard libs instead
- remove Know and Suff

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.

Stage work on fixing temporal_deep example (tools)

remove executable bit from text files in examples/

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