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