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
http://isabelle.in.tum.de/reports/Isabelle/report/5497697969e943bda524c4b01be7d12e
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.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
