On 03/06/16 18:49, David Matthews wrote: > The Poly/ML implementation was based on the idea that something called a > "multiple" ought to follow the usual rules of multiplication; nothing > stronger than that. I don't think I found anything that indicated what > the sign should be. The GCD code uses GMP's GCD if possible; the LCM > code is just derived from that. > > I have no strong opinions on this and I'm happy to change it. There's > also the question of whether to add it to the IntInf structure and > signature despite the incompatibility with the "official" library > definition.
How is the situation wrt. planned updates of the SML Basic Library specification? Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially, which a clear specification about the sign, whatever that might be. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev