Re: [isabelle] Separating function declaration from implementation

George Karabotsos writes:
 > Hello all,
 > I am wondering if there is a way to separate the declaration of a 
 > function (as defined by the fun or function keywords) by its implementation.
 > This is possible using the older consts and primrec or refdef way for 
 > declaring functions but I cannot see how it can be done with the new way.

I noticed this too, and to take it one step further, why can't the
syntactic outlines of these tools be similar; i.e. just replace
"primrec" with "function".  The reason I request this is that when
primrec fails (e.g. even on some primitive recursive functions in the
nominal package) I just switch to function.  Why should this require
changing more than one keyword?


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