Re: [isabelle] primrec



Viorel,

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
(http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/functions.pdf)
contains useful descriptions of the "fun" and "function" commands.

Kind regards,
Tjark







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