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
simplifier will use automatically. In addition, datatype and fun
plicitly declare some simplification rules: datatype the distinctness
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 jaist.ac.jp> a écrit:
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
Search for "fun primrec" here:
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and