src/Pure/General/rat.ML
changeset 19557 4866ebb16ba8
parent 17950 924d3e71cdc9
child 22189 10278e568741
--- a/src/Pure/General/rat.ML	Thu May 04 11:34:27 2006 +0200
+++ b/src/Pure/General/rat.ML	Thu May 04 12:50:01 2006 +0200
@@ -10,6 +10,7 @@
   type rat
   exception DIVZERO
   val zero: rat
+  val one: rat
   val rat_of_int: int -> rat
   val rat_of_intinf: IntInf.int -> rat
   val rat_of_quotient: IntInf.int * IntInf.int -> rat
@@ -40,6 +41,8 @@
 
 val zero = Rat (true, 0, 1);
 
+val one = Rat (true, 1, 1);
+
 fun rat_of_intinf i =
   if i < 0
   then Rat (false, ~i, 1)