23340

1 
(* Title: Pure/MLSystems/de_overload.ML


2 
ID: $Id$


3 
Author: Makarius


4 


5 
Deoverloaded 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.<=;
