# HG changeset patch
# User krauss
# Date 1227273702 -3600
# Node ID 381a3b3139ae2f2cfc79cc3153a4577a23d8d55b
# Parent  191cbfac6c9aadd3d6c0979ad85ee2b7076bb75b
added binary logarithm

diff -r 191cbfac6c9a -r 381a3b3139ae src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Fri Nov 21 13:17:43 2008 +0100
+++ b/src/Pure/General/integer.ML	Fri Nov 21 14:21:42 2008 +0100
@@ -16,6 +16,7 @@
   val gcds: int list -> int
   val lcm: int -> int -> int
   val lcms: int list -> int
+  val log: int -> int        (* binary logarithm *)
 end;
 
 structure Integer : INTEGER =
@@ -54,5 +55,10 @@
 fun lcm x y = (x * y) div (gcd x y);
 fun lcms xs = fold lcm xs 1;
 
+fun logr 1 a = a
+  | logr n a = logr (n div 2) (a + 1)
+
+fun log n = if n > 0 then logr n 0 else error "log: <= 0"
+
 end;