[isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9

Lukas Bulwahn bulwahn at in.tum.de
Thu Oct 13 10:55:34 CEST 2011

On 10/13/2011 10:52 AM, Florian Haftmann wrote:
> Hi Lukas,
> »removing checking of generated code because it fails on the mira
> testing infrastructure due to a missing Pure image« – I don't quite
> understand this.  Why exactly is the check failing?
> 	Florian
The issue can be observed at


Checking that the generated code in the Depth-First-Search AFP entry 
actually compiles with ML is a minor point anyway, so I did not dig into 
the details, but removed the check instead.


More information about the isabelle-dev mailing list