Make more build-related cleanups

Consistently use dehyphenated version of name to stand as
kernelid (i.e., "expk", "stdknl", "otknl", rather than anything with
leading hyphens). This requires change to Holmakefiles that wanted to
build OpenTheory articles when being executed under otknl.

Also make

build cleanAll

clean in all directories, not just those belonging to stdknl.

Add hol-words: OpenTheory package of src/n-bit

Empty command-line Holmake only builds first target in Holmakefile.

If there is no Holmakefile, or if there is a Holmakefile with no
targets, then the old behaviour of attempting to build everything
possible happens.

Documented in release notes and DESCRIPTION.

Many of the distribution's Holmakefiles were harmed in the creation of
this commit, but, for the reasons given in the release notes, I don't
think this should happen that often for typical user developments.

Closes #175

Make src/n-bit also clean its selftest.exe file

Add theorem WORD_MODIFY_BIT + other minor changes.

Add some dependencies.

Added a bit-blasting conversion: BBLAST_CONV. This goes beyond the
capabilities of WORD_BIT_EQ_CONV by expanding out additions / subtractions.
This allows the new conversion to automatically handle small but tricky bit
vector goals. For example:

``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)``

and

``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w``

(These aren't provable with wordsLib.WORD_DECIDE.)

Obviously bit-blasting is a brute force approach, so the new conversion should
be used with care. It will only work well for smallish word sizes and when
there is only and handful of additions around. It is also "eager" -- additions
are expanded out even when not strictly necessary. For example, in

``(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32``

the sum ``a + b`` is expanded. Users may be able to achieve speed-ups by first
introducing abbreviations and then proving general forms, e.g.

``x <+ c /\ c <+ d ==> x <+ d:word32``

The conversion handles most operators, however, the following are not covered /
interpreted:

-- Type variables for word lengths, i.e. terms of type ``:'a word``.

-- General multiplication, i.e. ``w1 * w2``. Multiplication by a literal is
okay, although this may introduce many additions.

-- Bit field selections with non-literal bounds, e.g. ``(exp1 -- exp2) w``.

-- Shifting by non-literal amounts, e.g. ``w << exp``.

-- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w.

-- word_div, word_sdiv, word_mod and word_log2.