--- a/src/HOL/Decision_Procs/approximation.ML Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML Fri Jan 01 17:08:51 2021 +0100
@@ -156,7 +156,7 @@
val (x, r) = Integer.div_mod m (Integer.pow (~e) 2)
- val p = ((if x = 0 then prec else prec - (IntInf.log2 x + 1)) * 3) div 10 + 1
+ val p = ((if x = 0 then prec else prec - (Integer.log2 x + 1)) * 3) div 10 + 1
val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0)
--- a/src/HOL/Matrix_LP/float_arith.ML Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Matrix_LP/float_arith.ML Fri Jan 01 17:08:51 2021 +0100
@@ -105,7 +105,7 @@
else
(exp5 (~ d), d)
- val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
+ val L = Real.floor (int2real (Integer.log2 q) + int2real r * ln2_10)
val L1 = L + 1
val (q1, r1) = subtract (q, r) (bin2dec L1)
--- a/src/HOL/Tools/Function/scnp_solve.ML Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML Fri Jan 01 17:08:51 2021 +0100
@@ -46,7 +46,7 @@
fun num_prog_pts (GP (arities, _)) = length arities ;
fun num_graphs (GP (_, gs)) = length gs ;
fun arity (GP (arities, gl)) i = nth arities i ;
-fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1
+fun ndigits (GP (arities, _)) = Integer.log2 (Integer.sum arities) + 1
(** Propositional formulas **)
--- 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));