# HG changeset patch
# User haftmann
# Date 1179073009 -7200
# Node ID 372e3471fca2233a4c0b1a90228341389e3bc18e
# Parent  cf78004a86f6e4b977baa4293a2d483db6f144b3
added module int

diff -r cf78004a86f6 -r 372e3471fca2 src/Pure/General/int.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/int.ML	Sun May 13 18:16:49 2007 +0200
@@ -0,0 +1,62 @@
+(*  Title:      Pure/General/int.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Unbounded integers.
+*)
+
+signature INTT =
+sig
+  type int
+  val zero: int
+  val one: int
+  val two: int
+  val int: Int.int -> int
+  val machine_int: int -> Int.int
+  val string_of_int: int -> string
+  val int_of_string: string -> int option
+  val eq: int * int -> bool
+  val cmp: int * int -> order
+  val le: int -> int -> bool
+  val cmp_zero: int -> order
+  val add: int -> int -> int
+  val sub: int -> int -> int
+  val mult: int -> int -> int
+  val divmod: int -> int -> int * int
+  val div: int -> int -> int
+  val mod: int -> int -> int
+  val neg: int -> int
+  val exp: int -> int
+end;
+
+structure Intt: INTT =
+struct
+
+open IntInf;
+
+val int = IntInf.fromInt;
+
+val zero = int 0;
+val one = int 1;
+val two = int 2;
+
+val machine_int = IntInf.toInt;
+val string_of_int = IntInf.toString;
+val int_of_string = IntInf.fromString;
+
+val eq = op =;
+val cmp = compare;
+val le = curry (op <=);
+val cmp_zero = curry cmp zero;
+val add = curry (op +);
+val sub = curry (op -);
+val mult = curry ( op * );
+val divmod = curry divMod;
+nonfix div
+val div = curry div;
+nonfix mod
+val mod = curry mod;
+val neg = IntInf.~;
+fun exp n = pow (2, IntInf.toInt n);
+
+end;