removed "log" again, as IntInf.log2 already exists.
--- a/src/Pure/General/integer.ML Mon Nov 24 18:05:20 2008 +0100
+++ b/src/Pure/General/integer.ML Mon Nov 24 20:12:23 2008 +0100
@@ -16,7 +16,6 @@
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 =
@@ -55,10 +54,5 @@
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;