# HG changeset patch
# User wenzelm
# Date 1181638876 -7200
# Node ID 57c6a46d9153b197bbc8f5a1482c273329ce2fca
# Parent  babddcf161ca7ffe1bad3182cacb01a621813563
De-overloaded operations for int and real.

diff -r babddcf161ca -r 57c6a46d9153 Admin/de_overload.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/de_overload.ML	Tue Jun 12 11:01:16 2007 +0200
@@ -0,0 +1,44 @@
+(*  Title:      Pure/ML-Systems/de_overload.ML
+    ID:         $Id$
+    Author:     Makarius
+
+De-overloaded operations for int and real.
+*)
+
+(* int *)
+
+val op + = Int.+;
+val op - = Int.-;
+val op * = Int.*;
+val op div = Int.div;
+val op mod = Int.mod;
+val ~ = Int.~;
+val abs = Int.abs;
+
+infix  7  *%
+infix  6  +% -%
+infix  4  >% >=% <% <=%
+
+val op *% = Int.*;
+val op +% = Int.+;
+val op -% = Int.-;
+val op >% = Int.>;
+val op >=% = Int.>=;
+val op <% = Int.<;
+val op <=% = Int.<=;
+
+
+(* real *)
+
+infix  7  *~ /~
+infix  6  +~ -~
+infix  4  >~ >=~ <~ <=~
+
+val op *~ = Real.*;
+val op /~ = Real./;
+val op +~ = Real.+;
+val op -~ = Real.-;
+val op >~ = Real.>;
+val op >=~ = Real.>=;
+val op <~ = Real.<;
+val op <=~ = Real.<=;