wenzelm@23340: (*  Title:      Pure/ML-Systems/de_overload.ML
wenzelm@23340:     ID:         $Id$
wenzelm@23340:     Author:     Makarius
wenzelm@23340: 
wenzelm@23340: De-overloaded operations for int and real.
wenzelm@23340: *)
wenzelm@23340: 
wenzelm@23340: (* int *)
wenzelm@23340: 
wenzelm@23340: val op + = Int.+;
wenzelm@23340: val op - = Int.-;
wenzelm@23340: val op * = Int.*;
wenzelm@23340: val op div = Int.div;
wenzelm@23340: val op mod = Int.mod;
wenzelm@23340: val ~ = Int.~;
wenzelm@23340: val abs = Int.abs;
wenzelm@23340: 
wenzelm@23340: infix  7  *%
wenzelm@23340: infix  6  +% -%
wenzelm@23340: infix  4  >% >=% <% <=%
wenzelm@23340: 
wenzelm@23340: val op *% = Int.*;
wenzelm@23340: val op +% = Int.+;
wenzelm@23340: val op -% = Int.-;
wenzelm@23340: val op >% = Int.>;
wenzelm@23340: val op >=% = Int.>=;
wenzelm@23340: val op <% = Int.<;
wenzelm@23340: val op <=% = Int.<=;
wenzelm@23340: 
wenzelm@23340: 
wenzelm@23340: (* real *)
wenzelm@23340: 
wenzelm@23340: infix  7  *~ /~
wenzelm@23340: infix  6  +~ -~
wenzelm@23340: infix  4  >~ >=~ <~ <=~
wenzelm@23340: 
wenzelm@23340: val op *~ = Real.*;
wenzelm@23340: val op /~ = Real./;
wenzelm@23340: val op +~ = Real.+;
wenzelm@23340: val op -~ = Real.-;
wenzelm@23340: val op >~ = Real.>;
wenzelm@23340: val op >=~ = Real.>=;
wenzelm@23340: val op <~ = Real.<;
wenzelm@23340: val op <=~ = Real.<=;