Email Gateway (Aug 23 2022 at 08:40): Email Gateway (Aug 23 2022 at 08:40):From: Dominique Unruh <unruh@ut.ee>
Hi,
when using "proof induction", I can use "case XXX" to refer to start
proving a specific case. All facts in this case are then available under
the name XXX, and the induction hypothesis under the name XXX.IH.
However, if my lemma contains == instead of = in the assumptions, then
the induction method still works, and the name XXX still contains all
facts, but XXX.IH is not defined.
This is illustrated by the attached theory (works with Isabelle2019 and
Isabelle2020-RC1).
Is this expected behavior? If so, what is the rationale?
Best wishes,
Dominique.
Scratch.thy
Last updated: Nov 21 2024 at 12:39 UTC