Stream: Beginner Questions

Topic: Isar for if-then-else

view this post on Zulip Gergely Buday (Aug 04 2020 at 13:19):

What is the Isar proof structure for a goal P( if condition then exprA else exprB) ?

view this post on Zulip Lukas Stevens (Aug 04 2020 at 13:58):

proof(cases "condition")

view this post on Zulip Gergely Buday (Aug 04 2020 at 14:32):

Thanks

Last updated: Mar 25 2026 at 05:23 UTC