# HG changeset patch
# User wenzelm
# Date 1464724450 -7200
# Node ID c583ca33076a7d4474c1c94666dc040acd94837c
# Parent  af562e9760380e67140763ec883fa6b319118d84
ad-hoc overloading for standard operations on type Rat.rat;

diff -r af562e976038 -r c583ca33076a NEWS
--- a/NEWS	Tue May 31 19:51:01 2016 +0200
+++ b/NEWS	Tue May 31 21:54:10 2016 +0200
@@ -344,8 +344,12 @@
   nn_integral :: 'a measure => ('a => ennreal) => ennreal
 INCOMPATIBILITY.
 
+
 *** ML ***
 
+* Ad-hoc overloading for standard operations on type Rat.rat: + - * / =
+< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
+
 * The ML function "ML" provides easy access to run-time compilation.
 This is particularly useful for conditional compilation, without
 requiring separate files.
diff -r af562e976038 -r c583ca33076a src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 21:54:10 2016 +0200
@@ -923,7 +923,7 @@
         val cr = dest_frac c
         val clt = Thm.dest_fun2 ct
         val cz = Thm.dest_arg ct
-        val neg = cr </ Rat.zero
+        val neg = cr < Rat.zero
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -946,7 +946,7 @@
         val cr = dest_frac c
         val clt = Thm.dest_fun2 ct
         val cz = Thm.dest_arg ct
-        val neg = cr </ Rat.zero
+        val neg = cr < Rat.zero
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -968,7 +968,7 @@
         val cr = dest_frac c
         val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
         val cz = Thm.dest_arg ct
-        val neg = cr </ Rat.zero
+        val neg = cr < Rat.zero
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -993,7 +993,7 @@
         val cr = dest_frac c
         val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
         val cz = Thm.dest_arg ct
-        val neg = cr </ Rat.zero
+        val neg = cr < Rat.zero
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
diff -r af562e976038 -r c583ca33076a src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 21:54:10 2016 +0200
@@ -39,7 +39,7 @@
  let fun pow r i =
    if i = 0 then rat_1 else
    let val d = pow r (i div 2)
-   in d */ d */ (if i mod 2 = 0 then rat_1 else r)
+   in d * d * (if i mod 2 = 0 then rat_1 else r)
    end
  in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
 
@@ -47,7 +47,7 @@
   let
     val (a,b) = Rat.quotient_of_rat (Rat.abs r)
     val d = a div b
-    val s = if r </ rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
+    val s = if r < rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
     val x2 = 2 * (a - (b * d))
   in s (if x2 >= b then d + 1 else d) end
 
@@ -78,22 +78,22 @@
 local
 
 fun normalize y =
-  if abs_rat y </ (rat_1 // rat_10) then normalize (rat_10 */ y) - 1
-  else if abs_rat y >=/ rat_1 then normalize (y // rat_10) + 1
+  if abs_rat y < (rat_1 / rat_10) then normalize (rat_10 * y) - 1
+  else if abs_rat y >= rat_1 then normalize (y / rat_10) + 1
   else 0
 
 in
 
 fun decimalize d x =
-  if x =/ rat_0 then "0.0"
+  if x = rat_0 then "0.0"
   else
     let
       val y = Rat.abs x
       val e = normalize y
-      val z = pow10(~ e) */ y +/ rat_1
-      val k = int_of_rat (round_rat(pow10 d */ z))
+      val z = pow10(~ e) * y + rat_1
+      val k = int_of_rat (round_rat(pow10 d * z))
     in
-      (if x </ rat_0 then "-0." else "0.") ^
+      (if x < rat_0 then "-0." else "0.") ^
       implode (tl (raw_explode(string_of_int k))) ^
       (if e = 0 then "" else "e" ^ string_of_int e)
     end
@@ -117,7 +117,7 @@
 
 type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
 
-fun iszero (_, r) = r =/ rat_0;
+fun iszero (_, r) = r = rat_0;
 
 
 (* Vectors. Conventionally indexed 1..n.                                     *)
@@ -128,8 +128,8 @@
 
 fun vector_cmul c (v: vector) =
   let val n = dim v in
-    if c =/ rat_0 then vector_0 n
-    else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
+    if c = rat_0 then vector_0 n
+    else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
   end;
 
 fun vector_of_list l =
@@ -151,7 +151,7 @@
 (* Monomials.                                                                *)
 
 fun monomial_eval assig m =
-  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
+  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
     m rat_1;
 
 val monomial_1 = FuncUtil.Ctermfunc.empty;
@@ -169,7 +169,7 @@
 (* Polynomials.                                                              *)
 
 fun eval assig p =
-  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
+  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p rat_0;
 
 val poly_0 = FuncUtil.Monomialfunc.empty;
 
@@ -180,28 +180,28 @@
 fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
 
 fun poly_const c =
-  if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
+  if c = rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
 
 fun poly_cmul c p =
-  if c =/ rat_0 then poly_0
-  else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p;
+  if c = rat_0 then poly_0
+  else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
 
 fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
 
 
 fun poly_add p1 p2 =
-  FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
+  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = rat_0) p1 p2;
 
 fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
 
 fun poly_cmmul (c,m) p =
-  if c =/ rat_0 then poly_0
+  if c = rat_0 then poly_0
   else
     if FuncUtil.Ctermfunc.is_empty m
-    then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p
+    then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p
     else
       FuncUtil.Monomialfunc.fold (fn (m', d) => fn a =>
-          (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
+          (FuncUtil.Monomialfunc.update (monomial_mul m m', c * d) a)) p poly_0;
 
 fun poly_mul p1 p2 =
   FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
@@ -323,10 +323,10 @@
 val numeral = Scan.one isnum
 val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
 val decimalfrac = Scan.repeat1 numeral
-  >> (fn s => rat_of_string(implode s) // pow10 (length s))
+  >> (fn s => rat_of_string(implode s) / pow10 (length s))
 val decimalsig =
   decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
-  >> (fn (h,NONE) => h | (h,SOME x) => h +/ x)
+  >> (fn (h,NONE) => h | (h,SOME x) => h + x)
 fun signed prs =
      $$ "-" |-- prs >> Rat.neg
   || $$ "+" |-- prs
@@ -337,7 +337,7 @@
 val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
 
 val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
-  >> (fn (h, x) => h */ pow10 (int_of_rat x));
+  >> (fn (h, x) => h * pow10 (int_of_rat x));
 
 fun mkparser p s =
   let val (x,rst) = p (raw_explode s)
@@ -359,7 +359,7 @@
 
 (* Version for (int*int*int) keys *)
 local
-  fun max_rat x y = if x </ y then y else x
+  fun max_rat x y = if x < y then y else x
   fun common_denominator fld amat acc =
     fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
   fun maximal_element fld amat acc =
@@ -374,24 +374,24 @@
   let
     val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
     val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
-    val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats
+    val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats
     val obj' = vector_cmul cd2 obj
     val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
     val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
     val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
     val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
-    val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats'
+    val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
     val obj'' = vector_cmul scal2 obj'
   in solver obj'' mats'' end
 end;
 
 (* Round a vector to "nice" rationals.                                       *)
 
-fun nice_rational n x = round_rat (n */ x) // n;
+fun nice_rational n x = round_rat (n * x) / n;
 fun nice_vector n ((d,v) : vector) =
   (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a =>
       let val y = nice_rational n c in
-        if c =/ rat_0 then a
+        if c = rat_0 then a
         else FuncUtil.Intfunc.update (i,y) a
       end) v FuncUtil.Intfunc.empty): vector
 
@@ -400,16 +400,16 @@
 (* Stuff for "equations" ((int*int*int)->num functions).                         *)
 
 fun tri_equation_cmul c eq =
-  if c =/ rat_0 then Inttriplefunc.empty
-  else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
+  if c = rat_0 then Inttriplefunc.empty
+  else Inttriplefunc.map (fn _ => fn d => c * d) eq;
 
 fun tri_equation_add eq1 eq2 =
-  Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
+  Inttriplefunc.combine (curry op +) (fn x => x = rat_0) eq1 eq2;
 
 fun tri_equation_eval assig eq =
   let
     fun value v = Inttriplefunc.apply assig v
-  in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0 end;
+  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq rat_0 end;
 
 (* Eliminate all variables, in an essentially arbitrary order.               *)
 
@@ -438,11 +438,11 @@
               val v = choose_variable eq
               val a = Inttriplefunc.apply eq v
               val eq' =
-                tri_equation_cmul ((Rat.rat_of_int ~1) // a) (Inttriplefunc.delete_safe v eq)
+                tri_equation_cmul ((Rat.rat_of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
               fun elim e =
                 let val b = Inttriplefunc.tryapplyd e v rat_0 in
-                  if b =/ rat_0 then e
-                  else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
+                  if b = rat_0 then e
+                  else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
                 end
             in
               eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
@@ -487,8 +487,8 @@
       let
         val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
       in
-        if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
-        else if a11 =/ rat_0 then
+        if a11 < rat_0 then raise Failure "diagonalize: not PSD"
+        else if a11 = rat_0 then
           if FuncUtil.Intfunc.is_empty (snd (row i m))
           then diagonalize n (i + 1) m
           else raise Failure "diagonalize: not PSD ___ "
@@ -497,7 +497,7 @@
             val v = row i m
             val v' =
               (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
-                let val y = c // a11
+                let val y = c / a11
                 in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
                 end) (snd v) FuncUtil.Intfunc.empty)
             fun upt0 x y a =
@@ -508,8 +508,8 @@
                 iter (i + 1, n) (fn j =>
                   iter (i + 1, n) (fn k =>
                     (upt0 (j, k)
-                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -/
-                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */
+                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -
+                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 *
                         FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
                     FuncUtil.Intpairfunc.empty)
           in (a11, v') :: diagonalize n (i + 1) m' end
@@ -603,10 +603,10 @@
 
 (* 3D versions of matrix operations to consider blocks separately.           *)
 
-val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
+val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = rat_0);
 fun bmatrix_cmul c bm =
-  if c =/ rat_0 then Inttriplefunc.empty
-  else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
+  if c = rat_0 then Inttriplefunc.empty
+  else Inttriplefunc.map (fn _ => fn x => c * x) bm;
 
 val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
 
@@ -803,13 +803,13 @@
         fun trivial_axiom (p, ax) =
           (case ax of
             RealArith.Axiom_eq n =>
-              if eval FuncUtil.Ctermfunc.empty p <>/ Rat.zero then nth eqs n
+              if eval FuncUtil.Ctermfunc.empty p <> Rat.zero then nth eqs n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | RealArith.Axiom_le n =>
-              if eval FuncUtil.Ctermfunc.empty p </ Rat.zero then nth les n
+              if eval FuncUtil.Ctermfunc.empty p < Rat.zero then nth les n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | RealArith.Axiom_lt n =>
-              if eval FuncUtil.Ctermfunc.empty p <=/ Rat.zero then nth lts n
+              if eval FuncUtil.Ctermfunc.empty p <= Rat.zero then nth lts n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | _ => error "trivial_axiom: Not a trivial axiom")
       in
diff -r af562e976038 -r c583ca33076a src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Tue May 31 21:54:10 2016 +0200
@@ -585,27 +585,27 @@
 
 (* A linear arithmetic prover *)
 local
-  val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
-  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
+  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
+  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
   val one_tm = @{cterm "1::real"}
   fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
      ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
        not(p(FuncUtil.Ctermfunc.apply e one_tm)))
 
   fun linear_ineqs vars (les,lts) =
-    case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
+    case find_first (contradictory (fn x => x > Rat.zero)) lts of
       SOME r => r
     | NONE =>
-      (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
+      (case find_first (contradictory (fn x => x > Rat.zero)) les of
          SOME r => r
        | NONE =>
          if null vars then error "linear_ineqs: no contradiction" else
          let
            val ineqs = les @ lts
            fun blowup v =
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
            val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
              (map (fn v => (v,blowup v)) vars)))
            fun addup (e1,p1) (e2,p2) acc =
@@ -613,7 +613,7 @@
                val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
                val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
              in
-               if c1 */ c2 >=/ Rat.zero then acc else
+               if c1 * c2 >= Rat.zero then acc else
                let
                  val e1' = linear_cmul (Rat.abs c2) e1
                  val e2' = linear_cmul (Rat.abs c1) e2
@@ -623,13 +623,13 @@
                end
              end
            val (les0,les1) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
            val (lts0,lts1) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
            val (lesp,lesn) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
            val (ltsp,ltsn) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
            val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
            val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
                       (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
@@ -637,7 +637,7 @@
          end)
 
   fun linear_eqs(eqs,les,lts) =
-    case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
+    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
       SOME r => r
     | NONE =>
       (case eqs of
@@ -651,9 +651,9 @@
            val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
            fun xform (inp as (t,q)) =
              let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
-               if d =/ Rat.zero then inp else
+               if d = Rat.zero then inp else
                let
-                 val k = (Rat.neg d) */ Rat.abs c // c
+                 val k = (Rat.neg d) * Rat.abs c / c
                  val e' = linear_cmul k e
                  val t' = linear_cmul (Rat.abs c) t
                  val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
diff -r af562e976038 -r c583ca33076a src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 21:54:10 2016 +0200
@@ -28,14 +28,14 @@
             find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
       | @{term "op * :: real => _"}$_$_ =>
             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
-            augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
+            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= Rat.zero)
                       (Thm.dest_arg t) acc
       | _ => augment_norm true t acc
 
  val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
  fun cterm_lincomb_cmul c t =
-    if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
- fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+    if c = Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
+ fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = Rat.zero) l r
  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
@@ -43,8 +43,8 @@
  val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
 *)
  fun int_lincomb_cmul c t =
-    if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
- fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+    if c = Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
+ fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = Rat.zero) l r
 (*
  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
@@ -84,7 +84,7 @@
 fun replacenegnorms cv t = case Thm.term_of t of
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ =>
-    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
+    if dest_ratconst (Thm.dest_arg1 t) < Rat.zero then arg_conv cv t else Thm.reflexive t
 | _ => Thm.reflexive t
 (*
 fun flip v eq =
@@ -96,7 +96,7 @@
 |(a::t) => let val res = allsubsets t in
                map (cons a) res @ res end
 fun evaluate env lin =
- FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
+ FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
    lin Rat.zero
 
 fun solve (vs,eqs) = case (vs,eqs) of
@@ -129,11 +129,11 @@
     NONE => NONE
    | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
-  val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
- in fold_rev (insert (eq_list op =/)) unset []
+  val unset = filter (forall (fn c => c >= Rat.zero)) rawvs
+ in fold_rev (insert (eq_list op =)) unset []
  end
 
-val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
+val subsumes = eq_list (fn (x, y) => Rat.abs x <= Rat.abs y)
 
 fun subsume todo dun = case todo of
  [] => dun
@@ -297,18 +297,18 @@
        fun check_solution v =
         let
           val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
-        in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
+        in forall (fn e => evaluate f e = Rat.zero) flippedequations
         end
        val goodverts = filter check_solution rawverts
        val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
-      in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
+      in map (map2 (fn s => fn c => Rat.rat_of_int s * c) signfixups) goodverts
       end
      val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
     in subsume allverts []
     end
    fun compute_ineq v =
     let
-     val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
+     val ths = map_filter (fn (v,t) => if v = Rat.zero then NONE
                                      else SOME(norm_cmul_rule v t))
                             (v ~~ nubs)
      fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
diff -r af562e976038 -r c583ca33076a src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue May 31 21:54:10 2016 +0200
@@ -80,14 +80,14 @@
   | (l1,[]) => l1
   | ((c1,m1)::o1,(c2,m2)::o2) =>
         if m1 = m2 then
-          let val c = c1+/c2 val rest = grob_add o1 o2 in
-          if c =/ rat_0 then rest else (c,m1)::rest end
+          let val c = c1 + c2 val rest = grob_add o1 o2 in
+          if c = rat_0 then rest else (c,m1)::rest end
         else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
         else (c2,m2)::(grob_add l1 o2);
 
 fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
 
-fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
+fun grob_mmul (c1,m1) (c2,m2) = (c1 * c2, ListPair.map (op +) (m1, m2));
 
 fun grob_cmul cm pol = map (grob_mmul cm) pol;
 
@@ -99,16 +99,16 @@
 fun grob_inv l =
   case l of
     [(c,vs)] => if (forall (fn x => x = 0) vs) then
-                  if (c =/ rat_0) then error "grob_inv: division by zero"
-                  else [(rat_1 // c,vs)]
+                  if (c = rat_0) then error "grob_inv: division by zero"
+                  else [(rat_1 / c,vs)]
               else error "grob_inv: non-constant divisor polynomial"
   | _ => error "grob_inv: non-constant divisor polynomial";
 
 fun grob_div l1 l2 =
   case l2 of
     [(c,l)] => if (forall (fn x => x = 0) l) then
-                 if c =/ rat_0 then error "grob_div: division by zero"
-                 else grob_cmul (rat_1 // c,l) l1
+                 if c = rat_0 then error "grob_div: division by zero"
+                 else grob_cmul (rat_1 / c,l) l1
              else error "grob_div: non-constant divisor polynomial"
   | _ => error "grob_div: non-constant divisor polynomial";
 
@@ -120,7 +120,7 @@
 (* Monomial division operation. *)
 
 fun mdiv (c1,m1) (c2,m2) =
-  (c1//c2,
+  (c1 / c2,
    map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
 
 (* Lowest common multiple of two monomials. *)
@@ -178,8 +178,8 @@
 fun monic (pol,hist) =
   if null pol then (pol,hist) else
   let val (c',m') = hd pol in
-  (map (fn (c,m) => (c//c',m)) pol,
-   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
+  (map (fn (c,m) => (c / c',m)) pol,
+   Mmul((rat_1 / c',map (K 0) m'),hist)) end;
 
 (* The most popular heuristic is to order critical pairs by LCM monomial.    *)
 
@@ -190,14 +190,14 @@
     (_,[]) => false
   | ([],_) => true
   | ((c1,m1)::o1,(c2,m2)::o2) =>
-        c1 </ c2 orelse
-        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
+        c1 < c2 orelse
+        c1 = c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
 
 fun align  ((p,hp),(q,hq)) =
   if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
 
 fun poly_eq p1 p2 =
-  eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
+  eq_list (fn ((c1, m1), (c2, m2)) => c1 = c2 andalso (m1: int list) = m2) (p1, p2);
 
 fun memx ((p1,_),(p2,_)) ppairs =
   not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
@@ -318,7 +318,7 @@
     let val cert = resolve_proof vars (grobner_refute pols)
         val l =
             fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
-        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
+        (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
 
 (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
 
@@ -608,7 +608,7 @@
      [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
 handle  CTERM _ =>
  ((let val x = dest_const tm
- in if x =/ rat_0 then [] else [(x,map (K 0) vars)]
+ in if x = rat_0 then [] else [(x,map (K 0) vars)]
  end)
  handle ERROR _ =>
   ((grob_neg(grobify_term vars (ring_dest_neg tm)))
@@ -712,9 +712,9 @@
        val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
       in (vars,l,cert,th2)
       end)
-    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
+    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > rat_0) p)) cert
     val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
-                                            (filter (fn (c,_) => c </ rat_0) p))) cert
+                                            (filter (fn (c,_) => c < rat_0) p))) cert
     val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
     val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
     fun thm_fn pols =
diff -r af562e976038 -r c583ca33076a src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Tue May 31 19:51:01 2016 +0200
+++ b/src/Pure/General/rat.ML	Tue May 31 21:54:10 2016 +0200
@@ -102,17 +102,13 @@
 
 end;
 
-infix 7 */ //;
-infix 6 +/ -/;
-infix 4 =/ </ <=/ >/ >=/ <>/;
-
-fun a +/ b = Rat.add a b;
-fun a -/ b = a +/ Rat.neg b;
-fun a */ b = Rat.mult a b;
-fun a // b = a */ Rat.inv b;
-fun a =/ b = Rat.eq (a, b);
-fun a </ b = Rat.lt a b;
-fun a <=/ b = Rat.le a b;
-fun a >/ b = b </ a;
-fun a >=/ b = b <=/ a;
-fun a <>/ b = not (a =/ b);
+ML_system_overload (uncurry Rat.add) "+";
+ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-";
+ML_system_overload (uncurry Rat.mult) "*";
+ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/";
+ML_system_overload Rat.eq "=";
+ML_system_overload (uncurry Rat.lt) "<";
+ML_system_overload (uncurry Rat.le) "<=";
+ML_system_overload (fn (a, b) => Rat.lt b a) ">";
+ML_system_overload (fn (a, b) => Rat.le b a) ">=";
+ML_system_overload (not o Rat.eq) "<>";