src/HOL/Library/positivstellensatz.ML
 changeset 67232 a00f5a71e672 parent 67091 1393c2340eec child 67267 c5994f1fa0fa
```     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:06:08 2017 +0100
1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:52:35 2017 +0100
1.3 @@ -370,8 +370,8 @@
1.4      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
1.5      fun oprconv cv ct =
1.6        let val g = Thm.dest_fun2 ct
1.7 -      in if g aconvc @{cterm "op <= :: real => _"}
1.8 -            orelse g aconvc @{cterm "op < :: real => _"}
1.9 +      in if g aconvc @{cterm "(op <=) :: real => _"}
1.10 +            orelse g aconvc @{cterm "(op <) :: real => _"}
1.11           then arg_conv cv ct else arg1_conv cv ct
1.12        end
1.13
1.14 @@ -406,13 +406,13 @@
1.15            | Axiom_le n => nth les n
1.16            | Axiom_lt n => nth lts n
1.17            | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
1.18 -                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
1.19 +                          (Thm.apply (Thm.apply @{cterm "(op =)::real => _"} (mk_numeric x))
1.20                                 @{cterm "0::real"})))
1.21            | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
1.22 -                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
1.23 +                          (Thm.apply (Thm.apply @{cterm "(op <=)::real => _"}
1.24                                       @{cterm "0::real"}) (mk_numeric x))))
1.25            | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
1.26 -                      (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
1.27 +                      (Thm.apply (Thm.apply @{cterm "(op <)::real => _"} @{cterm "0::real"})
1.28                          (mk_numeric x))))
1.29            | Square pt => square_rule (cterm_of_poly pt)
1.30            | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
1.31 @@ -428,9 +428,9 @@
1.32
1.33      val concl = Thm.dest_arg o Thm.cprop_of
1.34      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
1.35 -    val is_req = is_binop @{cterm "op =:: real => _"}
1.36 -    val is_ge = is_binop @{cterm "op <=:: real => _"}
1.37 -    val is_gt = is_binop @{cterm "op <:: real => _"}
1.38 +    val is_req = is_binop @{cterm "(op =):: real => _"}
1.39 +    val is_ge = is_binop @{cterm "(op <=):: real => _"}
1.40 +    val is_gt = is_binop @{cterm "(op <):: real => _"}
1.41      val is_conj = is_binop @{cterm HOL.conj}
1.42      val is_disj = is_binop @{cterm HOL.disj}
1.43      fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
1.44 @@ -476,7 +476,7 @@
1.45      fun dest_binary b ct =
1.46          if is_binop b ct then Thm.dest_binop ct
1.47          else raise CTERM ("dest_binary",[b,ct])
1.48 -    val dest_eq = dest_binary @{cterm "op = :: real => _"}
1.49 +    val dest_eq = dest_binary @{cterm "(op =) :: real => _"}
1.50      val neq_th = nth pth 5
1.51      fun real_not_eq_conv ct =
1.52        let
1.53 @@ -486,8 +486,8 @@
1.54          val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
1.55          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
1.56          val th' = Drule.binop_cong_rule @{cterm HOL.disj}
1.57 -          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
1.58 -          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
1.59 +          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_p)
1.60 +          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_n)
1.61        in Thm.transitive th th'
1.62        end
1.63      fun equal_implies_1_rule PQ =
```