added binary logarithm

--- 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;