# HG changeset patch
# User nipkow
# Date 1513803155 -3600
# Node ID a00f5a71e672688a26c9024125462862025c3a19
# Parent  754952c12293f4e439853e0cf283aa4fe115fc1d
tuned op's

diff -r 754952c12293 -r a00f5a71e672 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:06:08 2017 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:52:35 2017 +0100
@@ -370,8 +370,8 @@
     fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
     fun oprconv cv ct =
       let val g = Thm.dest_fun2 ct
-      in if g aconvc @{cterm "op <= :: real => _"}
-            orelse g aconvc @{cterm "op < :: real => _"}
+      in if g aconvc @{cterm "(op <=) :: real => _"}
+            orelse g aconvc @{cterm "(op <) :: real => _"}
          then arg_conv cv ct else arg1_conv cv ct
       end
 
@@ -406,13 +406,13 @@
           | Axiom_le n => nth les n
           | Axiom_lt n => nth lts n
           | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
-                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
+                          (Thm.apply (Thm.apply @{cterm "(op =)::real => _"} (mk_numeric x))
                                @{cterm "0::real"})))
           | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
-                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
+                          (Thm.apply (Thm.apply @{cterm "(op <=)::real => _"}
                                      @{cterm "0::real"}) (mk_numeric x))))
           | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
-                      (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
+                      (Thm.apply (Thm.apply @{cterm "(op <)::real => _"} @{cterm "0::real"})
                         (mk_numeric x))))
           | Square pt => square_rule (cterm_of_poly pt)
           | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
@@ -428,9 +428,9 @@
 
     val concl = Thm.dest_arg o Thm.cprop_of
     fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
-    val is_req = is_binop @{cterm "op =:: real => _"}
-    val is_ge = is_binop @{cterm "op <=:: real => _"}
-    val is_gt = is_binop @{cterm "op <:: real => _"}
+    val is_req = is_binop @{cterm "(op =):: real => _"}
+    val is_ge = is_binop @{cterm "(op <=):: real => _"}
+    val is_gt = is_binop @{cterm "(op <):: real => _"}
     val is_conj = is_binop @{cterm HOL.conj}
     val is_disj = is_binop @{cterm HOL.disj}
     fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
@@ -476,7 +476,7 @@
     fun dest_binary b ct =
         if is_binop b ct then Thm.dest_binop ct
         else raise CTERM ("dest_binary",[b,ct])
-    val dest_eq = dest_binary @{cterm "op = :: real => _"}
+    val dest_eq = dest_binary @{cterm "(op =) :: real => _"}
     val neq_th = nth pth 5
     fun real_not_eq_conv ct =
       let
@@ -486,8 +486,8 @@
         val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
         val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
         val th' = Drule.binop_cong_rule @{cterm HOL.disj}
-          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
-          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
+          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_p)
+          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_n)
       in Thm.transitive th th'
       end
     fun equal_implies_1_rule PQ =