[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

> On 7 Jun 2015, at 07:38, Dmitriy Traytel <traytel at in.tum.de> wrote:
> 
> I'm not sure if this is something for the repository though, since it has a factor of >2 impact on the build-time:

Thanks for investigating. But how do we explain this?

Possibly “fun” insists on converting on creating unconditional patterns only, while “recdef” allows conditional equations. But one could easily insert conditions manually in order to simplify the set of patterns. There are 14 instances of recdef in Cooper.thy. Do any of them stand out as extra slow?

Larry

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/1e91e492/attachment-0002.html>