*** ML ***
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
(notably for big integers). Subtle change of semantics: Integer.gcd and
Integer.lcm both normalize the sign, results are never negative. This
coincides with the definitions in HOL/GCD.thy. INCOMPATIBILITY.
This refers to Isabelle/d3ed7f00e818.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
