src/Pure/basis.ML
changeset 5208 cea0adbc7276
parent 5021 235f8508d440
child 5643 983ce1421211
     1.1 --- a/src/Pure/basis.ML	Tue Jul 28 16:59:15 1998 +0200
     1.2 +++ b/src/Pure/basis.ML	Tue Jul 28 17:02:41 1998 +0200
     1.3 @@ -42,6 +42,19 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +structure Real =
     1.8 +  struct
     1.9 +  fun toString (x: real) = makestring x;
    1.10 +  fun max (x, y) = if x < y then y else x : real;
    1.11 +  fun min (x, y) = if x < y then x else y : real;
    1.12 +  val real = real;
    1.13 +  val floor = floor;
    1.14 +  fun ceil x = ~1 - floor (~ (x + 1.0));
    1.15 +  fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
    1.16 +  fun trunc x = if x < 0.0 then ceil x else floor x;
    1.17 +  end;
    1.18 +
    1.19 +
    1.20  structure List =
    1.21    struct
    1.22    exception Empty