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