Fix minor bug in behaviour of EVERY_CONJ_CONV (with selftest)
Fix arithmetic d.p. mis-feature identified in c59783a4d0e3d

Issue was that conditional expressions with non-presburger guards
resulted in goals that weren't provable because ARITH couldn't handle
boolean sub-terms that weren't presburger. This prevented its
instance-generalisation mechanism from solving obvious goals like that
in the test-case.

Now the instance-generalisation mechanism will perform up to four
case-splits on boolean sub-terms. Of course, the choice of four is
completely arbitrary, but a possible 32-fold expansion in goal-size
seems unreasonable.

Document the change in the release notes.
Make depedencies of numheap on arith code more explicit.

This will cause the "bossLib heap" to get rebuilt as well because an
updated numheap will cause every subsequent theory to get rebuilt,
triggering a rebuild of hol.builder.
Fix fiddly proof broken by my change in 04f5254.

It was this fiddliness that made me identify the problem fixed in
04f5254 as a problem at all.