refactor hol-light in preparation for direct stateful semantics

The code for the ITP'14 submission now mostly lives in
hol-light/stateless (and hol-light/set-theory). The plan is to make a
new version in hol-light/stateful.