Re: [isabelle] lemmas following from inductive definitions



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

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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