Stream: Beginner Questions

Topic: ✔ Calculation proofs have unintuitive behavior


view this post on Zulip isauser (Feb 24 2026 at 19:44):

I think it would still be good to document these issues and/or the errors that may show up due to them. The "No matching trans rules for calculation" error was my fault and makes sense in retrospective, but "Vacuous calculation result" isn't listed in the Isar reference manual nor or at https://isabelle.systems/cookbook/, and the only search result in google is a mailing list thread that points to another thread (that the website doesn't allow you to access).

view this post on Zulip Notification Bot (Feb 24 2026 at 19:44):

isauser has marked this topic as resolved.


Last updated: Mar 04 2026 at 20:34 UTC