[isabelle] lemmas following from inductive definitions




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






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