`temporal_deep` fixes, selftests and reformats (#792)

* Fixed translationsLib due to eqtype changes

* Fixes for tight equality

* Turned ltl2omega.sml into a selftest

* Trying to fix ltl_to_automaton_formulaTheory for tight equality

* BUECHO -> BUECHI

* Do not run selftest.exe normally

* Simplified type definitions using abbreviations

* reformated with more comments

* reformated

* Fixed Holmakefile in examples

* Turning modelCheck.sml into a Moscow ML-only selftest

* re-formated the entire symbolic_kripke_structureTheory

* Added a selftest from modelCheck.sml without using modelCheckLib

* More cleanups

* More cleanups

* stage work commenting symbolic_semi_automatonTheory

* Commenting automaton_formulaTheory

* Commenting automaton_formulaTheory

* Commenting automaton_formulaTheory

* Commented automaton_formulaTheory

* Commented symbolic_kripke_structureTheory

* Reviewed/commented full_ltlTheory

* Fixed trailing whitespaces, prepared for submitting

* Fixed references

* Fixed comments in automaton_formulaTheory

* Removed 100+ extra empty lines, done here

rename ltlTheory -> full_ltlTheory

In order to avoid a name clash with "examples/logic/ltl/ltl" the theory
"examples/temporal_deep/src/deep_embeddings/ltl" was renamed to
"full_ltl"

temporal_deep: fix translationsLib

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