What is the Isar proof structure for a goal P( if condition then exprA else exprB) ?
proof(cases "condition")
Thanks
Last updated: Sep 04 2025 at 16:26 UTC