*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: [isabelle] more Isabelle2007 conversion pains*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Tue, 27 May 2008 11:48:34 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <483A7E0B.60902@in.tum.de>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com> <48240A4F.1070006@in.tum.de> <48278BA3.6090206@nicta.com.au> <48325DC2.9080904@rsise.anu.edu.au> <483A7E0B.60902@in.tum.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

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 anumber 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, butin 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,

Regards, Jeremy

**Follow-Ups**:**Re: [isabelle] more Isabelle2007 conversion pains***From:*berghofe

**References**:**[isabelle] Reasoning about k-fold cartesian products***From:*Denis Bueno

**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Tobias Nipkow

**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Michael Norrish

**[isabelle] lemmas following from inductive definitions***From:*Jeremy Dawson

**Re: [isabelle] lemmas following from inductive definitions***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] journals on theorem proving
- Next by Date: [isabelle] Question to Sledgehammer output
- Previous by Thread: Re: [isabelle] lemmas following from inductive definitions
- Next by Thread: Re: [isabelle] more Isabelle2007 conversion pains
- Cl-isabelle-users May 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list