Re: [isabelle] Fun vs Primrec: difference?

Dear Yannick,

this is not the first time this question is asked. Maybe it is best to read through the previous discussions and come back if still questions remain:

Search for "fun primrec" here:



On 07/29/2012 03:33 AM, Yannick Duchêne (Hibou57) wrote:
Hi people out there,

New beginner here, and so beginner's questions :-P

My first one: what's the difference between “fun” and “primrec” please ?
Both looks similar or synonymous, but surprisingly, when Main is not
imported (yes, I know it should, but that's for testing), “fun” seems
not available.

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