[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
http://isabelle.in.tum.de/polyml-5.2.1/
Makarius
More information about the isabelle-dev
mailing list