[isabelle-dev] PolyML update

Makarius makarius at sketis.net
Sun Aug 13 12:57:58 CEST 2017


On 11/08/17 22:59, Makarius wrote:
> 
> Poly/ML 5.7 does not work for Isabelle
> 
> In the meantime, David Matthews has revised many things, so it probably
> works again, but it needs systematic testing on all platforms and
> 32/64bit combinations.

I have made some experiments with the Poly/ML repository version
938336aeb7eb from 02-Aug-2017, but it does not quite work (problem with
HOL-Decision_Procs).

David Matthews is in the middle of substantial changes again, so this is
probably to be expected.


	Makarius



More information about the isabelle-dev mailing list