Jakub Gonera (Mar 20 2026 at 20:57): Jakub Gonera (Mar 20 2026 at 20:57):I noticed multiple times a situation in JEdit where when I write out an Isar step ("have ...") in a proof and dispatch sledgehammer I get a warning saying "Derived "False" from these facts alone: ..." which vanishes when sledgehammer stops running.
Is this a (known) bug? Or should Isabelle be trusted when it says that the project became inconsistent, even if the warning does not persist?
I'm using Isabelle 2025-2.
Mathias Fleury (Mar 20 2026 at 21:00):in my experience it usually means that the theorem you are writing is wrong
Mathias Fleury (Mar 20 2026 at 21:00):for example by having contradictory assumptions
Mathias Fleury (Mar 20 2026 at 21:01):It is useful to click on the proof and see what the dependencies are
Mathias Fleury (Mar 20 2026 at 21:02):if the proof goes through, you know it is not a bug
Last updated: Apr 09 2026 at 09:11 UTC