Add a [path_induction_hammer] tactic

It's a more powerful version of [path_induction], but doesn't have very
good computational behavior.  It's somewhat tuned for speed, but is
unfortunately rather fiddly, speed-wise.

This closes #173.