Admin/de_overload.ML
author haftmann
Tue Jul 10 17:30:50 2007 +0200 (2007-07-10)
changeset 23709 fd31da8f752a
parent 23340 57c6a46d9153
child 24584 01e83ffa6c54
permissions -rw-r--r--
moved lfp_induct2 here
wenzelm@23340
     1
(*  Title:      Pure/ML-Systems/de_overload.ML
wenzelm@23340
     2
    ID:         $Id$
wenzelm@23340
     3
    Author:     Makarius
wenzelm@23340
     4
wenzelm@23340
     5
De-overloaded operations for int and real.
wenzelm@23340
     6
*)
wenzelm@23340
     7
wenzelm@23340
     8
(* int *)
wenzelm@23340
     9
wenzelm@23340
    10
val op + = Int.+;
wenzelm@23340
    11
val op - = Int.-;
wenzelm@23340
    12
val op * = Int.*;
wenzelm@23340
    13
val op div = Int.div;
wenzelm@23340
    14
val op mod = Int.mod;
wenzelm@23340
    15
val ~ = Int.~;
wenzelm@23340
    16
val abs = Int.abs;
wenzelm@23340
    17
wenzelm@23340
    18
infix  7  *%
wenzelm@23340
    19
infix  6  +% -%
wenzelm@23340
    20
infix  4  >% >=% <% <=%
wenzelm@23340
    21
wenzelm@23340
    22
val op *% = Int.*;
wenzelm@23340
    23
val op +% = Int.+;
wenzelm@23340
    24
val op -% = Int.-;
wenzelm@23340
    25
val op >% = Int.>;
wenzelm@23340
    26
val op >=% = Int.>=;
wenzelm@23340
    27
val op <% = Int.<;
wenzelm@23340
    28
val op <=% = Int.<=;
wenzelm@23340
    29
wenzelm@23340
    30
wenzelm@23340
    31
(* real *)
wenzelm@23340
    32
wenzelm@23340
    33
infix  7  *~ /~
wenzelm@23340
    34
infix  6  +~ -~
wenzelm@23340
    35
infix  4  >~ >=~ <~ <=~
wenzelm@23340
    36
wenzelm@23340
    37
val op *~ = Real.*;
wenzelm@23340
    38
val op /~ = Real./;
wenzelm@23340
    39
val op +~ = Real.+;
wenzelm@23340
    40
val op -~ = Real.-;
wenzelm@23340
    41
val op >~ = Real.>;
wenzelm@23340
    42
val op >=~ = Real.>=;
wenzelm@23340
    43
val op <~ = Real.<;
wenzelm@23340
    44
val op <=~ = Real.<=;