  Inductive theorem proving is an important long-standing challenge in computer
science. In this extended abstract, we first summarize the recent developments
of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a
novel approach to further automating inductive theorem proving. Upon success,
united reasoning takes the best of three schools of reasoning: deductive
reasoning, inductive reasoning, and inductive reasoning, to prove difficult
inductive problems automatically.
