Remove uses of global grammar from some library files

Uses of Q.prove dodge redefinitions of the Parse structure, and end up
using the surrounding global grammar. For this reason, it's best not
to use Q in library implementations.

Remove eqtype declaration for term type

Update bitstringLib.extract_v2w_CONV.

Should have been included in commit 7c45d79.

Add Conv.memoize.

This can be used to build conversions that lookup previous result in a red-black tree.

The n-bit libraries are updated to make use of Conv.memoize and new functions in computeLib.

Add a new conversion and simpset fragment for bit-strings.

Opening lcsymtacs is no longer necessary.

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Support building custom compsets that cover bitstringTheory and integer_wordTheory.

Generalise bitstringLib.word_bit_CONV.

Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence.

Includes some tidying-up work.

This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib.

This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.

Performance tweak to bitstringLib.v2n_CONV.

Minor change to exception reporting in bitstringLib.

Add WORD_BIT_INDEX_CONV and tweak word_bit_CONV.

Update some syntax files to use HolKernel.syntax_fns.

Avoid messages appearing when loading bitstringLib.

Fix for bitstringLib, which was broken during work on Issue #70.

Minor tweaks to various conversions under src/n-bit.

Add a theory of bit-strings, which defines word operations over ``:bool list``. The maps "v2w" and "w2v" provide a connection to fixed-width bit vectors.