From: Peter Lammich <lammich@in.tum.de>
Hi all,
Isar-proof reconstruction from sledgehammer proposes a vacuous proof
(that, obviously, doesn't not work). Example below. Posting it here, as
this is the first time that I see such a 'proof' proposed by
sledgehammer, so maybe 2021-1 regression.
Last updated: Jan 04 2025 at 20:18 UTC