Is there an easy way to specify logical dichotomy/trichotomy (ie exactly one of P,Q,R holds)?
If so, is there an intro rule for its cases?
You might want to check out the command ˋconsiderˋ, e.g. in the Isabelle/Isar reference manual.
Maximilian Schaeffeler said:
You might want to check out the command ˋconsiderˋ, e.g. in the Isabelle/Isar reference manual.
Perfect just what I wanted
Last updated: Dec 21 2024 at 12:33 UTC