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.

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.

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