--- a/src/HOL/Library/positivstellensatz.ML Thu Feb 01 17:21:58 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Thu Feb 01 17:27:13 2018 +0100
@@ -365,8 +365,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>\<open>((\<le>)) :: real \<Rightarrow> _\<close>
- orelse g aconvc \<^cterm>\<open>((<)) :: real \<Rightarrow> _\<close>
+ in if g aconvc \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>
+ orelse g aconvc \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
then arg_conv cv ct else arg1_conv cv ct
end
@@ -401,13 +401,13 @@
| Axiom_le n => nth les n
| Axiom_lt n => nth lts n
| Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
- (Thm.apply (Thm.apply \<^cterm>\<open>((=))::real \<Rightarrow> _\<close> (mk_numeric x))
+ (Thm.apply (Thm.apply \<^cterm>\<open>(=)::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>((\<le>))::real \<Rightarrow> _\<close>
+ (Thm.apply (Thm.apply \<^cterm>\<open>(\<le>)::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>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
+ (Thm.apply (Thm.apply \<^cterm>\<open>(<)::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)
@@ -423,9 +423,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>\<open>((=)):: real \<Rightarrow> _\<close>
- val is_ge = is_binop \<^cterm>\<open>((\<le>)):: real \<Rightarrow> _\<close>
- val is_gt = is_binop \<^cterm>\<open>((<)):: real \<Rightarrow> _\<close>
+ val is_req = is_binop \<^cterm>\<open>(=):: real \<Rightarrow> _\<close>
+ val is_ge = is_binop \<^cterm>\<open>(\<le>):: real \<Rightarrow> _\<close>
+ val is_gt = is_binop \<^cterm>\<open>(<):: 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})
@@ -471,7 +471,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>\<open>((=)) :: real \<Rightarrow> _\<close>
+ val dest_eq = dest_binary \<^cterm>\<open>(=) :: real \<Rightarrow> _\<close>
val neq_th = nth pth 5
fun real_not_eq_conv ct =
let
@@ -481,8 +481,8 @@
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>\<open>HOL.disj\<close>
- (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
- (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
+ (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(<)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
+ (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(<)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
in Thm.transitive th th'
end
fun equal_implies_1_rule PQ =