--- a/src/Pure/library.ML Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/library.ML Sat Oct 30 16:33:58 2010 +0200
@@ -130,6 +130,10 @@
val read_int: string list -> int * string list
val oct_char: string -> string
+ (*reals*)
+ val string_of_real: real -> string
+ val signed_string_of_real: real -> string
+
(*strings*)
val nth_string: string -> int -> string
val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
@@ -668,6 +672,15 @@
+(** reals **)
+
+val string_of_real = Real.fmt (StringCvt.GEN NONE);
+
+fun signed_string_of_real x =
+ if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
+
+
+
(** strings **)
(* functions tuned for strings, avoiding explode *)