[isabelle-dev] Remaining uses of defer_recdef?

Larry Paulson lp15 at cam.ac.uk
Sun Jun 7 19:20:06 CEST 2015

> 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?


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

More information about the isabelle-dev mailing list