Re: [isabelle] primrec


On Wed, 2011-11-09 at 10:55 +0200, Viorel Preoteasa wrote:
> I will use "fun". I was afraid that using fun
> would require providing the well founded
> relation which ensures termination.
> However it seems that in this case Isabelle
> figures it out automatically.

The Tutorial on Function Definitions
contains useful descriptions of the "fun" and "function" commands.

Kind regards,

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