  In this paper, we investigate the potential of the Boyer-Moore waterfall
model for the automation of inductive proofs within a modern proof assistant.
We analyze the basic concepts and methodology underlying this 30-year-old model
and implement a new, fully integrated tool in the theorem prover HOL Light that
can be invoked as a tactic. We also describe several extensions and
enhancements to the model. These include the integration of existing HOL Light
proof procedures and the addition of state-of-the-art generalization techniques
into the waterfall. Various features, such as proof feedback and heuristics
dealing with non-termination, that are needed to make this automated tool
useful within our interactive setting are also discussed. Finally, we present a
thorough evaluation of the approach using a set of 150 theorems, and discuss
the effectiveness of our additions and relevance of the model in light of our
results.
