I tried to use the
sledgehammer command in Isabelle/HOL (2021) after the
proof command, and got an error:
Illegal application of proof command in "state" mode
If I use it before the Isar
proof command, then
sledgehammer works. My question is:
proof generates several sub-goals, having proved the first sub-goal somehow, is there a way to use
sledgehammer in the middle of the
proof process to try to prove the other sub-goals?
The more general question is:
sledgehammer designed for the old tactics and not suitable for use inside Isar proofs.
(I first asked this in SO; but did not get a definitive answer. Therefore, I am posting the question here, and deleting it there).