[isabelle] Separating function declaration from implementation

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.


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