src/Pure/library.ML
changeset 15965 f422f8283491
parent 15760 1ca99038c847
child 15970 b8855873d234
     1.1 --- a/src/Pure/library.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -117,8 +117,8 @@
     1.4    val suffixes1: 'a list -> 'a list list
     1.5  
     1.6    (*integers*)
     1.7 -  val gcd: int * int -> int
     1.8 -  val lcm: int * int -> int
     1.9 +  val gcd: IntInf.int * IntInf.int -> IntInf.int
    1.10 +  val lcm: IntInf.int * IntInf.int -> IntInf.int
    1.11    val inc: int ref -> int
    1.12    val dec: int ref -> int
    1.13    val upto: int * int -> int list
    1.14 @@ -136,13 +136,14 @@
    1.15    (*rational numbers*)
    1.16    type rat
    1.17    exception RAT of string
    1.18 -  val rep_rat: rat -> int * int
    1.19 +  val rep_rat: rat -> IntInf.int * IntInf.int
    1.20    val ratadd: rat * rat -> rat
    1.21    val ratmul: rat * rat -> rat
    1.22    val ratinv: rat -> rat
    1.23 -  val int_ratdiv: int * int -> rat
    1.24 +  val int_ratdiv: IntInf.int * IntInf.int -> rat
    1.25    val ratneg: rat -> rat
    1.26    val rat_of_int: int -> rat
    1.27 +  val rat_of_intinf: IntInf.int -> rat
    1.28  
    1.29    (*strings*)
    1.30    val nth_elem_string: int * string -> string
    1.31 @@ -665,7 +666,7 @@
    1.32  (** integers **)
    1.33  
    1.34  fun gcd(x,y) =
    1.35 -  let fun gxd x y =
    1.36 +  let fun gxd x y : IntInf.int =
    1.37      if y = 0 then x else gxd y (x mod y)
    1.38    in if x < y then gxd y x else gxd x y end;
    1.39  
    1.40 @@ -1186,7 +1187,7 @@
    1.41  
    1.42  (** rational numbers **)
    1.43  
    1.44 -datatype rat = Rat of bool * int * int
    1.45 +datatype rat = Rat of bool * IntInf.int * IntInf.int
    1.46  
    1.47  exception RAT of string;
    1.48  
    1.49 @@ -1212,7 +1213,9 @@
    1.50  
    1.51  fun ratneg(Rat(b,p,q)) = Rat(not b,p,q);
    1.52  
    1.53 -fun rat_of_int i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
    1.54 +fun rat_of_intinf i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
    1.55 +
    1.56 +fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
    1.57  
    1.58  
    1.59  (** misc **)