[isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

Makarius makarius at sketis.net
Sat Dec 10 16:32:42 CET 2016

On 08/12/16 17:41, David Matthews wrote:
> On 08/12/2016 15:01, Florian Haftmann wrote:
>> Hi all,
>> when testing polyml-test-7a7b742897e9 I found out that this breaks
>> session Algebraic_Numbers in the AFP:
>> *** At command "value" (line 42 of
>> "/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
>> *** exception Div raised (line 302 of "./basis/InitialBasis.ML")
>> It looks like a change in the semantics of integer division in PolyML,
>> but this is entirely speculative.
> No, it was a bug in the testing version of Poly/ML.  Thanks for pointing
> it out and in particular including the line number which allowed me to
> see immediately what was wrong.  Hopefully the commit I've just pushed
> will have fixed it.

This works, see


More information about the isabelle-dev mailing list