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 =