changeset 2141 | c2aedd8169cd |
parent 1480 | 85ecd3439e01 |
child 2242 | fa8c6c695a97 |
--- a/src/Pure/POLY.ML Wed Oct 30 11:21:24 1996 +0100 +++ b/src/Pure/POLY.ML Fri Nov 01 15:12:21 1996 +0100 @@ -9,6 +9,13 @@ open PolyML ExtendedIO; +structure Int = + struct + fun max (x, y) = if x < y then y else x : int; + fun min (x, y) = if x < y then x else y : int; + end; + + (*A conditional timing function: applies f to () and, if the flag is true, prints its runtime.*)