| changeset 63209 | 82cd1d481eb9 |
| parent 63208 | 3251e9dfea91 |
| child 63210 | a0685d2b420b |
--- a/src/Pure/General/rat.ML Wed Jun 01 15:33:45 2016 +0200 +++ b/src/Pure/General/rat.ML Wed Jun 01 16:02:02 2016 +0200 @@ -108,3 +108,5 @@ ML_system_overload (fn (a, b) => Rat.lt b a) ">"; ML_system_overload (fn (a, b) => Rat.le b a) ">="; ML_system_overload (not o Rat.eq) "<>"; + +ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));