# HG changeset patch
# User wenzelm
# Date 1513978771 -3600
# Node ID c5994f1fa0fa1b8f76f512701937957351ed44ec
# Parent  bf41a57e159fa077df09acaf6f35fe73e626fbe8
more symbols;

diff -r bf41a57e159f -r c5994f1fa0fa src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Fri Dec 22 21:23:06 2017 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Fri Dec 22 22:39:31 2017 +0100
@@ -184,23 +184,23 @@
 
 val pth_final = @{lemma "(\<not>p \<Longrightarrow> False) \<Longrightarrow> p" by blast}
 val pth_add =
-  @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and
-    "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and
-    "(x >= 0 ==> y >= 0 ==> x + y >= 0)" and "(x >= 0 ==> y > 0 ==> x + y > 0)" and
-    "(x > 0 ==> y = 0 ==> x + y > 0)" and "(x > 0 ==> y >= 0 ==> x + y > 0)" and
-    "(x > 0 ==> y > 0 ==> x + y > 0)" by simp_all};
+  @{lemma "(x = (0::real) \<Longrightarrow> y = 0 \<Longrightarrow> x + y = 0 )" and "( x = 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y \<ge> 0)" and
+    "(x = 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" and "(x \<ge> 0 \<Longrightarrow> y = 0 \<Longrightarrow> x + y \<ge> 0)" and
+    "(x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y \<ge> 0)" and "(x \<ge> 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" and
+    "(x > 0 \<Longrightarrow> y = 0 \<Longrightarrow> x + y > 0)" and "(x > 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y > 0)" and
+    "(x > 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" by simp_all};
 
 val pth_mul =
-  @{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0)" and "(x = 0 ==> y >= 0 ==> x * y = 0)" and
-    "(x = 0 ==> y > 0 ==> x * y = 0)" and "(x >= 0 ==> y = 0 ==> x * y = 0)" and
-    "(x >= 0 ==> y >= 0 ==> x * y >= 0)" and "(x >= 0 ==> y > 0 ==> x * y >= 0)" and
-    "(x > 0 ==>  y = 0 ==> x * y = 0)" and "(x > 0 ==> y >= 0 ==> x * y >= 0)" and
-    "(x > 0 ==>  y > 0 ==> x * y > 0)"
+  @{lemma "(x = (0::real) \<Longrightarrow> y = 0 \<Longrightarrow> x * y = 0)" and "(x = 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y = 0)" and
+    "(x = 0 \<Longrightarrow> y > 0 \<Longrightarrow> x * y = 0)" and "(x \<ge> 0 \<Longrightarrow> y = 0 \<Longrightarrow> x * y = 0)" and
+    "(x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y \<ge> 0)" and "(x \<ge> 0 \<Longrightarrow> y > 0 \<Longrightarrow> x * y \<ge> 0)" and
+    "(x > 0 \<Longrightarrow>  y = 0 \<Longrightarrow> x * y = 0)" and "(x > 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y \<ge> 0)" and
+    "(x > 0 \<Longrightarrow>  y > 0 \<Longrightarrow> x * y > 0)"
   by (auto intro: mult_mono[where a="0::real" and b="x" and d="y" and c="0", simplified]
     mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])};
 
-val pth_emul = @{lemma "y = (0::real) ==> x * y = 0"  by simp};
-val pth_square = @{lemma "x * x >= (0::real)"  by simp};
+val pth_emul = @{lemma "y = (0::real) \<Longrightarrow> x * y = 0"  by simp};
+val pth_square = @{lemma "x * x \<ge> (0::real)"  by simp};
 
 val weak_dnf_simps =
   List.take (@{thms simp_thms}, 34) @
@@ -289,15 +289,15 @@
   let
     val (a, b) = Rat.dest x
   in
-    if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
-    else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
-      (Numeral.mk_cnumber @{ctyp "real"} a))
-      (Numeral.mk_cnumber @{ctyp "real"} b)
+    if b = 1 then Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a
+    else Thm.apply (Thm.apply \<^cterm>\<open>op / :: real \<Rightarrow> _\<close>
+      (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a))
+      (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> b)
   end;
 
 fun dest_ratconst t =
   case Thm.term_of t of
-    Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+    Const(\<^const_name>\<open>divide\<close>, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
   | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
 fun is_ratconst t = can dest_ratconst t
 
@@ -324,30 +324,30 @@
 
 (* Map back polynomials to HOL.                         *)
 
-fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x)
-  (Numeral.mk_cnumber @{ctyp nat} k)
+fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply \<^cterm>\<open>op ^ :: real \<Rightarrow> _\<close> x)
+  (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> k)
 
 fun cterm_of_monomial m =
-  if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"}
+  if FuncUtil.Ctermfunc.is_empty m then \<^cterm>\<open>1::real\<close>
   else
     let
       val m' = FuncUtil.dest_monomial m
       val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
-    in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
+    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>op * :: real \<Rightarrow> _\<close> s) t) vps
     end
 
 fun cterm_of_cmonomial (m,c) =
   if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   else if c = @1 then cterm_of_monomial m
-  else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
+  else Thm.apply (Thm.apply \<^cterm>\<open>op *::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
 
 fun cterm_of_poly p =
-  if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"}
+  if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
   else
     let
       val cms = map cterm_of_cmonomial
         (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
-    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
+    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply \<^cterm>\<open>op + :: real \<Rightarrow> _\<close> t1) t2) cms
     end;
 
 (* A general real arithmetic prover *)
@@ -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>\<open>(op <=) :: real \<Rightarrow> _\<close>
+            orelse g aconvc \<^cterm>\<open>(op <) :: real \<Rightarrow> _\<close>
          then arg_conv cv ct else arg1_conv cv ct
       end
 
@@ -405,14 +405,14 @@
             Axiom_eq n => nth eqs n
           | 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))
-                               @{cterm "0::real"})))
-          | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
-                          (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"})
+          | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
+                          (Thm.apply (Thm.apply \<^cterm>\<open>(op =)::real \<Rightarrow> _\<close> (mk_numeric x))
+                               \<^cterm>\<open>0::real\<close>)))
+          | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
+                          (Thm.apply (Thm.apply \<^cterm>\<open>(op <=)::real \<Rightarrow> _\<close>
+                                     \<^cterm>\<open>0::real\<close>) (mk_numeric x))))
+          | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
+                      (Thm.apply (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
                         (mk_numeric x))))
           | Square pt => square_rule (cterm_of_poly pt)
           | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
@@ -428,11 +428,11 @@
 
     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_conj = is_binop @{cterm HOL.conj}
-    val is_disj = is_binop @{cterm HOL.disj}
+    val is_req = is_binop \<^cterm>\<open>(op =):: real \<Rightarrow> _\<close>
+    val is_ge = is_binop \<^cterm>\<open>(op <=):: real \<Rightarrow> _\<close>
+    val is_gt = is_binop \<^cterm>\<open>(op <):: real \<Rightarrow> _\<close>
+    val is_conj = is_binop \<^cterm>\<open>HOL.conj\<close>
+    val is_disj = is_binop \<^cterm>\<open>HOL.disj\<close>
     fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
     fun disj_cases th th1 th2 =
       let
@@ -443,8 +443,8 @@
           else error "disj_cases : conclusions not alpha convertible"
       in Thm.implies_elim (Thm.implies_elim
           (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
-          (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
-        (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
+          (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> p) th1))
+        (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> q) th2)
       end
     fun overall cert_choice dun ths =
       case ths of
@@ -466,28 +466,28 @@
             let
               val (th1, cert1) =
                 overall (Left::cert_choice) dun
-                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
+                  (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg1 ct))::oths)
               val (th2, cert2) =
                 overall (Right::cert_choice) dun
-                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
+                  (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg ct))::oths)
             in (disj_cases th th1 th2, Branch (cert1, cert2)) end
           else overall cert_choice (th::dun) oths
         end
     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>\<open>(op =) :: real \<Rightarrow> _\<close>
     val neq_th = nth pth 5
     fun real_not_eq_conv ct =
       let
         val (l,r) = dest_eq (Thm.dest_arg ct)
-        val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th
+        val th = Thm.instantiate ([],[((("x", 0), \<^typ>\<open>real\<close>),l),((("y", 0), \<^typ>\<open>real\<close>),r)]) neq_th
         val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
-        val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
+        val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> 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)
+        val th' = Drule.binop_cong_rule \<^cterm>\<open>HOL.disj\<close>
+          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
+          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
       in Thm.transitive th th'
       end
     fun equal_implies_1_rule PQ =
@@ -500,7 +500,7 @@
       let
         fun h (acc, t) =
           case Thm.term_of t of
-            Const(@{const_name Ex},_)$Abs(_,_,_) =>
+            Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
               h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
@@ -514,24 +514,24 @@
     fun mk_forall x th =
       let
         val T = Thm.typ_of_cterm x
-        val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
+        val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
       in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
 
     val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
 
-    fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
+    fun ext T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
     fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
 
     fun choose v th th' =
       case Thm.concl_of th of
-        @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
+        \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
         let
           val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
           val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
           val th0 = fconv_rule (Thm.beta_conversion true)
             (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
           val pv = (Thm.rhs_of o Thm.beta_conversion true)
-            (Thm.apply @{cterm Trueprop} (Thm.apply p v))
+            (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
           val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
         in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
       | _ => raise THM ("choose",0,[th, th'])
@@ -539,13 +539,13 @@
     fun simple_choose v th =
       choose v
         (Thm.assume
-          ((Thm.apply @{cterm Trueprop} o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
+          ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
 
     val strip_forall =
       let
         fun h (acc, t) =
           case Thm.term_of t of
-            Const(@{const_name All},_)$Abs(_,_,_) =>
+            Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
               h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
@@ -555,27 +555,27 @@
       let
         val nnf_norm_conv' =
           nnf_conv ctxt then_conv
-          literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
+          literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
           (Conv.cache_conv
             (first_conv [real_lt_conv, real_le_conv,
                          real_eq_conv, real_not_lt_conv,
                          real_not_le_conv, real_not_eq_conv, all_conv]))
-        fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
+        fun absremover ct = (literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
                   (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
                   try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
-        val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
+        val nct = Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close> ct)
         val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
         val tm0 = Thm.dest_arg (Thm.rhs_of th0)
         val (th, certificates) =
-          if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
+          if tm0 aconvc \<^cterm>\<open>False\<close> then (equal_implies_1_rule th0, Trivial) else
           let
             val (evs,bod) = strip_exists tm0
             val (avs,ibod) = strip_forall bod
-            val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
+            val th1 = Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (fold mk_forall avs (absremover ibod))
             val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
             val th3 =
               fold simple_choose evs
-                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
+                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> bod))) th2)
           in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
           end
       in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
@@ -587,7 +587,7 @@
 local
   val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
   fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
-  val one_tm = @{cterm "1::real"}
+  val one_tm = \<^cterm>\<open>1::real\<close>
   fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
      ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
        not(p(FuncUtil.Ctermfunc.apply e one_tm)))
@@ -673,7 +673,7 @@
     end
 
   fun lin_of_hol ct =
-    if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
+    if ct aconvc \<^cterm>\<open>0::real\<close> then FuncUtil.Ctermfunc.empty
     else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
     else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
     else
@@ -683,9 +683,9 @@
         else
           let val (opr,l) = Thm.dest_comb lop
           in
-            if opr aconvc @{cterm "op + :: real =>_"}
+            if opr aconvc \<^cterm>\<open>op + :: real \<Rightarrow> _\<close>
             then linear_add (lin_of_hol l) (lin_of_hol r)
-            else if opr aconvc @{cterm "op * :: real =>_"}
+            else if opr aconvc \<^cterm>\<open>op * :: real \<Rightarrow> _\<close>
                     andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
             else FuncUtil.Ctermfunc.onefunc (ct, @1)
           end
@@ -693,8 +693,8 @@
 
   fun is_alien ct =
     case Thm.term_of ct of
-      Const(@{const_name "of_nat"}, _)$ n => not (can HOLogic.dest_number n)
-    | Const(@{const_name "of_int"}, _)$ n => not (can HOLogic.dest_number n)
+      Const(\<^const_name>\<open>of_nat\<close>, _)$ n => not (can HOLogic.dest_number n)
+    | Const(\<^const_name>\<open>of_int\<close>, _)$ n => not (can HOLogic.dest_number n)
     | _ => false
 in
 fun real_linear_prover translator (eq,le,lt) =
@@ -724,15 +724,15 @@
 
   val absmaxmin_elim_conv2 =
     let
-      val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
-      val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
-      val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
-      val abs_tm = @{cterm "abs :: real => _"}
-      val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
-      val x_v = (("x", 0), @{typ real})
-      val y_v = (("y", 0), @{typ real})
-      val is_max = is_binop @{cterm "max :: real => _"}
-      val is_min = is_binop @{cterm "min :: real => _"}
+      val pth_abs = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] abs_split'
+      val pth_max = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] max_split
+      val pth_min = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] min_split
+      val abs_tm = \<^cterm>\<open>abs :: real \<Rightarrow> _\<close>
+      val p_v = (("P", 0), \<^typ>\<open>real \<Rightarrow> bool\<close>)
+      val x_v = (("x", 0), \<^typ>\<open>real\<close>)
+      val y_v = (("y", 0), \<^typ>\<open>real\<close>)
+      val is_max = is_binop \<^cterm>\<open>max :: real \<Rightarrow> _\<close>
+      val is_min = is_binop \<^cterm>\<open>min :: real \<Rightarrow> _\<close>
       fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
       fun eliminate_construct p c tm =
         let
@@ -772,7 +772,7 @@
     fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
     val {add, mul, neg, pow = _, sub = _, main} =
         Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
-        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
+        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
         simple_cterm_ord
   in gen_real_arith ctxt
      (cterm_of_rat,