[isabelle-dev] Speed of @{thm}

[Makarius]

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.


 	Makarius