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 http://isabelle.in.tum.de/repos/isabelle/rev/d23b7c9b9dd4 Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
