Re: [isabelle] Fun vs Primrec: difference?

Additionally, “isabelle2012/doc/prog-prove.pdf” also says on page 18

The attribute simp declares theorems to be simplification rules, which the simplifier will use automatically. In addition, datatype and fun commands im- plicitly declare some simplification rules: datatype the distinctness and injec-
  tivity rules, fun the defining equations.

But this does not implies primrec don't too. Will check a later day.

Le Sun, 29 Jul 2012 07:11:59 +0200, Christian Sternagel <c-sterna at> a écrit:

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:

“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.