removed "log" again, as IntInf.log2 already exists.
authorkrauss
Mon, 24 Nov 2008 20:12:23 +0100
changeset 28882 57bfd0fdea09
parent 28881 df2525ad10c6
child 28883 0f5b1accfb94
removed "log" again, as IntInf.log2 already exists.
src/Pure/General/integer.ML
--- 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;