Re: [isabelle] Case names for induct with datatypes



On Wed, 21 May 2008, Andreas Lochbihler wrote:

> I have a datatype which has a recursive constructor where the recursive 
> parameter is packed into another datatype, e.g. datatype T = ... | C "T 
> list"

> Does induct give case names to them at all?

Yes, print_cases will tell you the names produced by the datatype rule.


	Makarius






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