From: Peter Lammich <lammich@in.tum.de>
Hello Tobias (cc list).
Getting the following warning (during sledgehammer), with the message
to please inform Tobias ... here you are.
I cannot reproduce the warning in an isolated example, as sledgehammer
seems to find+reconstruct a different proof there, and no warning is
issued.
Last updated: Dec 21 2024 at 16:20 UTC