# HG changeset patch
# User wenzelm
# Date 901638161 -7200
# Node ID cea0adbc7276757dcf1fd7840cb429f2fca06498
# Parent  dd4f51adfff3646bb1dbb52438dfa942dce74059
added Real structure (taken from SML/NJ basis lib);

diff -r dd4f51adfff3 -r cea0adbc7276 src/Pure/basis.ML
--- a/src/Pure/basis.ML	Tue Jul 28 16:59:15 1998 +0200
+++ b/src/Pure/basis.ML	Tue Jul 28 17:02:41 1998 +0200
@@ -42,6 +42,19 @@
   end;
 
 
+structure Real =
+  struct
+  fun toString (x: real) = makestring x;
+  fun max (x, y) = if x < y then y else x : real;
+  fun min (x, y) = if x < y then x else y : real;
+  val real = real;
+  val floor = floor;
+  fun ceil x = ~1 - floor (~ (x + 1.0));
+  fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
+  fun trunc x = if x < 0.0 then ceil x else floor x;
+  end;
+
+
 structure List =
   struct
   exception Empty