# HG changeset patch
# User wenzelm
# Date 1189947509 -7200
# Node ID 4a6607412b40b65e47ad2c54c5a38fe6c4215185
# Parent  5877b88f262c9a49e4e7d485e73686c532b2182c
obsolete;

diff -r 5877b88f262c -r 4a6607412b40 Admin/de_overload.ML
--- a/Admin/de_overload.ML	Sun Sep 16 14:55:48 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*  Title:      Admin/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.<=;