[isabelle] Fun vs Primrec: difference?

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.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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