where I'm at

I've done a first draft of the technical section, with the part about
shifting and stability missing.

Notable changes:

- no more syntactic category for "local" assertions. Instead, we should
  introduce them in the text as "formulas without subjective views",
  which is clear enough.

- negation is back. we need it for P\cap Q |- emp, and also it's weird
  not to have negation (eg, do we then include \forall quantification
  separately?) Transformations that did not take negation into account
  (in the appendix/tech rep) should be adapted to deal with it, or
  mention that they cannot explicitly.

- uppercase for \lass{P}, which now prints P

- some text about actions vs rely and guarantee conditions. Perhaps this
  is now redundant with the intro

I'm trying to finish at least the shifting rules section tonight.