Connect Hets to SMV model checker (full integration)

[till]

• write parser for temporal logic syntax
• write abstract syntax, parser and printer for muSMV model syntax
• write an instance for logic Temporal of type class Logic (see source:trunk/Logic/Logic.hs, see source:trunk/Propositional/Logic_Propositional.hs)
• integrate muSMV as a prover in Hets (see source:trunk/Logic/Prover.hs)

first complete #518