[isabelle-dev] Speed of @{thm}

Makarius makarius at sketis.net
Sun Aug 12 21:28:43 CEST 2012

On Sun, 12 Aug 2012, Jasmin Blanchette wrote:

> Dmitriy noticed that performance decreased significantly when he moved 
> his ML code from ".thy" files to ".ML" files, probably because he had 
> many smaller "ML {* *}" blocks before.

OK, keep me informed when you find other things.  There are always limits 
of what the system can do, but it helps to know where they are, and 
sometimes the border can be pushed a bit further.


More information about the isabelle-dev mailing list