Add extension points for nil primitive

This commit adds nil to the basic operations of the plugin interface,
like apply and diff.

This implies adding various other related components, and adding
implementations for Nehemiah.

This operation is not yet used anywhere - in particular, the algebra of
changes still has a fixed definition, so proofs need not be
altered *yet*.

More extension points will be added later.
More extension points for proof plugin
Stop assuming nil v is v ⊟ v
Make nil an extension point in change algebra

This defines nil changes for groups as their identity element, and
updates nil changes also for Nehemiah (since this plugin uses group
changes for its base types).
nilt ↦ onil

onil is more coherent with ⊕ and ⊝.
Merge pull request #5 from inc-lc/topic/nil-extension

Add extension points for nil