Artem Khovanov (Jul 15 2022 at 19:30): Artem Khovanov (Jul 15 2022 at 19:30):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?
Maximilian Schaeffeler (Jul 15 2022 at 19:56):You might want to check out the command ˋconsiderˋ, e.g. in the Isabelle/Isar reference manual.
Artem Khovanov (Jul 15 2022 at 20:15):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