Don't use MATCH_MP

Make impl_tac work with universally quantified implications

Implement impl_{keep_,}tac with new provehyp_then primitive

The underlying primitive allows obvious generalisations of the impl
tactics, such as pulling from assumptions and passing the resulting
theorems to different continuation thm-tactics.

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

More moving lcsymtacs implementations elsewhere

Eventually lcsymtacs will just be a bunch of 'open' declarations, and
then people won't bother to include it at all.

More assorted code tidying.

Change src/bool to src/1 as a prelude to experimentation!