src/Pure/General/rat.ML
changeset 63209 82cd1d481eb9
parent 63208 3251e9dfea91
child 63210 a0685d2b420b
equal deleted inserted replaced
63208:3251e9dfea91 63209:82cd1d481eb9
   106 ML_system_overload (uncurry Rat.lt) "<";
   106 ML_system_overload (uncurry Rat.lt) "<";
   107 ML_system_overload (uncurry Rat.le) "<=";
   107 ML_system_overload (uncurry Rat.le) "<=";
   108 ML_system_overload (fn (a, b) => Rat.lt b a) ">";
   108 ML_system_overload (fn (a, b) => Rat.lt b a) ">";
   109 ML_system_overload (fn (a, b) => Rat.le b a) ">=";
   109 ML_system_overload (fn (a, b) => Rat.le b a) ">=";
   110 ML_system_overload (not o Rat.eq) "<>";
   110 ML_system_overload (not o Rat.eq) "<>";
       
   111 
       
   112 ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));