[isabelle-dev] NEWS: Rat in Isabelle/ML

Makarius makarius at sketis.net
Wed Jun 1 22:04:27 CEST 2016

On 01/06/16 21:47, Lawrence Paulson wrote:
> Doesn’t Poly/ML include an option to support GCDs (if not rationals) efficiently?

Do you mean PolyML.IntInf.gcd and PolyML.IntInf.lcm? That is already
used (da38571dd5bd).

These operations normally use GNU MP, but on Mac OS X only the old
builtin bigints of Poly/ML. (I still don't know how to compile Poly/ML
with libgmp such that the binary becomes self-contained.)


More information about the isabelle-dev mailing list