Email Gateway (Aug 18 2022 at 11:54): Email Gateway (Aug 18 2022 at 11:54):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
I'm trying to port some of my work from Isabelle2005 to Isabelle2007.
Where in Isabelle2005 I do an inductive definition and as a result a
number of theorems are produced, including elim and elims,
in Isabelle2007, (after changing these to "inductive_set" definitions)
the theorems elim and elims are missing.
In one example there is a theorem similar to elim called cases, but in
the other example there is nothing, apparently, in place of elims.
Where can I find these theorems?
Jeremy
Email Gateway (Aug 18 2022 at 11:56):From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
Dear Jeremy,
this is explained in the section about inductive(_set) in the NEWS file:
- The elimination or case analysis rules for (mutually) inductive
sets or predicates are now called "p_1.cases" ... "p_k.cases". The
list of rules "p_1_..._p_k.elims" is no longer available.
Greetings,
Stefan
Last updated: Nov 21 2024 at 12:39 UTC