diff -r 8bbe57116d13 -r a497f621bfd4 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Aug 06 18:06:56 2005 +0200
+++ b/src/Pure/library.ML	Sun Aug 07 12:28:10 2005 +0200
@@ -144,6 +144,10 @@
   type rat
   exception RAT of string
   val rep_rat: rat -> IntInf.int * IntInf.int
+  val ratge0: rat -> bool
+  val ratgt0: rat -> bool
+  val ratle: rat * rat -> bool
+  val ratlt: rat * rat -> bool
   val ratadd: rat * rat -> rat
   val ratmul: rat * rat -> rat
   val ratinv: rat -> rat
@@ -151,6 +155,7 @@
   val ratneg: rat -> rat
   val rat_of_int: int -> rat
   val rat_of_intinf: IntInf.int -> rat
+  val rat0: rat
 
   (*strings*)
   val nth_elem_string: int * string -> string
@@ -1224,6 +1229,7 @@
 
 
 (** rational numbers **)
+(* Keep them normalized! *)
 
 datatype rat = Rat of bool * IntInf.int * IntInf.int
 
@@ -1236,9 +1242,27 @@
       val m = gcd(absp,q)
   in Rat(a = (0 <= p), absp div m, q div m) end;
 
-fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
+fun ratcommon(p,q,r,s) =
   let val den = lcm(q,s)
-      val p = p*(den div q) and r = r*(den div s)
+  in (p*(den div q), r*(den div s), den) end
+
+fun ratge0(Rat(a,p,q)) = a;
+fun ratgt0(Rat(a,p,q)) = a andalso p > 0;
+
+fun ratle(Rat(a,p,q),Rat(b,r,s)) =
+  not a andalso b orelse
+  a = b andalso
+    let val (p,r,_) = ratcommon(p,q,r,s)
+    in if a then p <= r else r <= p end
+
+fun ratlt(Rat(a,p,q),Rat(b,r,s)) =
+  not a andalso b orelse
+  a = b andalso
+    let val (p,r,_) = ratcommon(p,q,r,s)
+    in if a then p < r else r < p end
+
+fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
+  let val (p,q,den) = ratcommon(p,q,r,s)
       val num = (if a then p else ~p) + (if b then r else ~r)
   in ratnorm(true,num,den) end;
 
@@ -1255,6 +1279,7 @@
 
 fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
 
+val rat0 = rat_of_int 0; 
 
 (** misc **)