Fix syntax error in Holmakefile

Fix temporal_deep Holmakefiles for new behaviours of multi-dir Holmake

I don't have any problems with these fixes (i.e., I'm happy to be
changing Holmake's behaviour, and not supporting what made these files
work previously):
- PolyML Holmake's dependency analysis gets confused by bvec.sml in
examples/muddy (the special Moscow ML keyword prim_type messes it
up) and so we alter model_check's Holmakefile to not include muddy
or HolBdd (which wants muddy)
- It is not enough to simply INCLUDES = directories that one wants
built in a top-level Holmakefile; the standard behaviour is to build
only enough to support the targets in the current directory. If a
directory has nothing in it (except sub-directories, say), then it
will do nothing. To get everything built in sub-directories, you
need the -r option, which can be passed in the Holmakefiles'
CLINE_OPTIONS variable. (Note though that Holmake clean in these
directories will now clean recursively too; perhaps the two meanings
of -r is a mistake; or perhaps one should be able to get
recursive-clean and recursive-build separately.)
- Having a target called clean is bad if every target is getting built
under a -r option. The only behaviour of this clean target was to
recursively call Holmake (itself a mistake), so I'm more than happy
to simply remove this.

Add DEFAULT_TARGETS to base variable environment for Holmake

Allows for much more concise presentation of standard pattern when
additional targets are required, namely:

all: $(DEFAULT_TARGETS) mytarget1 mytarget2
.PHONY: all

Fix up many examples of previous verbose style.

Thanks to Magnus for the suggestion.

Closes #618

Get temporal_deep/src/model_check to build by fixing Holmakefile

Added self tests

Fixed modelCheckLib with NuSMV model checker

remove executable bit from text files in examples/

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