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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and