Add a [path_induction_hammer] tactic

It's a more powerful version of [path_induction], but doesn't have very
good computational behavior.

This closes #173.