I have refactored the early parts of the paper:

- Added a section preliminaries.tex which should contain material
  we take for granted, e.g. bisimulation.

- I've split elAndBang.tex into two parts elAndBangCore.tex and
  elAndBangMore.tex. The former contains the core definitions
  (formulae, models, proof rules, soundness, completeness, standard
  translation etc).  The latter is for more advanced stuff like
  decision procedures, HML theorem etc. T

This is preliminary, and needs more work. I have not touched later
chapers.