> On 7 Jun 2015, at 07:38, Dmitriy Traytel <tray...@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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
