Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-1-RC3. Odd sledgehammer proof rec...


view this post on Zulip Email Gateway (Nov 13 2021 at 23:33):

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: Jul 15 2022 at 23:21 UTC