[isabelle] more Isabelle2007 conversion pains
Stefan Berghofer wrote:
Jeremy Dawson wrote:
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?
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.
thanks. But I now find a similar problem: the theorems x.mono, x.unfold
seem to have disappeared. Actually it seems the theorems x.mono,
x.unfold already don't appear in Isabelle2005 for new-style theory
files, but you could use an old-style theory file, or (sometimes) derive
x.unfold from x.defs.
But in Isabelle2007 you can't use an old-style theory file and even
x.defs doesn't seem to exist. Where have all these theorems gone?
This archive was generated by a fusion of
Pipermail (Mailman edition) and