[isabelle-dev] `compiling' the cookbook

Makarius makarius at sketis.net
Wed Mar 18 22:00:51 CET 2009

On Wed, 18 Mar 2009, urban at math.lmu.de wrote:

> No, it is supposed to take less than a minute, but
> it needs PolyML 5.2.1. My guess is that you compiling it
> with something else.

> For the time being, I can show you how to disable this
> example (it is in the file TimeLimit.thy) and for the
> future I will think of a better example to illustrate
> this function.

BTW, you can get Poly/ML 5.2.1 from 


More information about the isabelle-dev mailing list