[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?

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

Stefan,

thanks. But I now find a similar problem: the theorems x.mono, x.unfold and x.defs 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?

Regards,

Jeremy







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.