[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