Admin/de_overload.ML
author wenzelm
Tue, 24 Jul 2007 19:44:32 +0200
changeset 23961 9e7e1e309ebd
parent 23340 57c6a46d9153
child 24584 01e83ffa6c54
permissions -rw-r--r--
Multithreading in Poly/ML (version 5.1).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23340
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/de_overload.ML
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     4
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     5
De-overloaded operations for int and real.
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     6
*)
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     7
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     8
(* int *)
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
     9
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    10
val op + = Int.+;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    11
val op - = Int.-;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    12
val op * = Int.*;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    13
val op div = Int.div;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    14
val op mod = Int.mod;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    15
val ~ = Int.~;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    16
val abs = Int.abs;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    17
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    18
infix  7  *%
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    19
infix  6  +% -%
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    20
infix  4  >% >=% <% <=%
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    21
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    22
val op *% = Int.*;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    23
val op +% = Int.+;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    24
val op -% = Int.-;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    25
val op >% = Int.>;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    26
val op >=% = Int.>=;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    27
val op <% = Int.<;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    28
val op <=% = Int.<=;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    29
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    30
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    31
(* real *)
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    32
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    33
infix  7  *~ /~
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    34
infix  6  +~ -~
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    35
infix  4  >~ >=~ <~ <=~
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    36
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    37
val op *~ = Real.*;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    38
val op /~ = Real./;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    39
val op +~ = Real.+;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    40
val op -~ = Real.-;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    41
val op >~ = Real.>;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    42
val op >=~ = Real.>=;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    43
val op <~ = Real.<;
57c6a46d9153 De-overloaded operations for int and real.
wenzelm
parents:
diff changeset
    44
val op <=~ = Real.<=;