move HOL semantics and metatheory into separate directory

to make room for the implementations
slight reorganise again: separate syntax from semantics

this way, the implementation doesn't have to depend on the semantics
directory.
start version of monadic functions for the new HOL

the verification script is broken, but hasn't been looked at yet