src/Tools/integer.ML
changeset 24633 0a3a02066244
parent 24632 779fc4fcbf8b
child 24634 38db11874724
--- a/src/Tools/integer.ML	Tue Sep 18 17:53:37 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      Tools/integer.ML
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-
-Unbounded integers.
-*)
-
-signature INTEGER =
-sig
-  val sign: int -> order
-  val sum: int list -> int
-  val div_mod: int -> int -> int * int
-  val square: int -> int
-  val pow: int -> int -> int (* exponent -> base -> result *)
-  val gcd: int -> int -> int
-  val gcds: int list -> int
-  val lcm: int -> int -> int
-  val lcms: int list -> int
-end;
-
-structure Integer : INTEGER =
-struct
-
-fun sign x = int_ord (x, 0);
-
-fun sum xs = fold (curry op +) xs 0;
-
-fun div_mod x y = IntInf.divMod (x, y);
-
-fun square x = x * x;
-
-fun pow k l =
-  let
-    fun pw 0 _ = 1
-      | pw 1 l = l
-      | pw k l =
-          let
-            val (k', r) = div_mod k 2;
-            val l' = pw k' (l * l);
-          in if r = 0 then l' else l' * l end;
-  in
-    if k < 0
-    then error "pow: negative exponent"
-    else pw k l
-  end;
-
-fun gcd x y =
-  let
-    fun gxd x y = if y = 0 then x else gxd y (x mod y)
-  in if x < y then gxd y x else gxd x y end;
-
-fun gcds xs = fold gcd xs 0;
-
-fun lcm x y = (x * y) div (gcd x y);
-fun lcms xs = fold lcm xs 1;
-
-end;
-