--- a/src/Pure/General/integer.ML Tue Dec 29 16:42:01 2020 +0100
+++ b/src/Pure/General/integer.ML Fri Jan 01 17:08:51 2021 +0100
@@ -16,6 +16,7 @@
val div_mod: int -> int -> int * int
val square: int -> int
val pow: int -> int -> int (* exponent -> base -> result *)
+ val log2: int -> int
val gcd: int -> int -> int
val lcm: int -> int -> int
val gcds: int list -> int
@@ -44,6 +45,8 @@
fun pow k l = IntInf.pow (l, k);
+val log2 = IntInf.log2;
+
fun gcd x y = PolyML.IntInf.gcd (x, y);
fun lcm x y = abs (PolyML.IntInf.lcm (x, y));