src/HOL/Library/positivstellensatz.ML
 changeset 63211 0bec0d1d9998 parent 63205 97b721666890 child 63648 f9f3006a5579
```     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 17:46:12 2016 +0200
1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 19:23:18 2016 +0200
1.3 @@ -615,10 +615,10 @@
1.4               in
1.5                 if c1 * c2 >= @0 then acc else
1.6                 let
1.7 -                 val e1' = linear_cmul (Rat.abs c2) e1
1.8 -                 val e2' = linear_cmul (Rat.abs c1) e2
1.9 -                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
1.10 -                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
1.11 +                 val e1' = linear_cmul (abs c2) e1
1.12 +                 val e2' = linear_cmul (abs c1) e2
1.13 +                 val p1' = Product(Rational_lt (abs c2), p1)
1.14 +                 val p2' = Product(Rational_lt (abs c1), p2)
1.16                 end
1.17               end
1.18 @@ -653,11 +653,11 @@
1.19               let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
1.20                 if d = @0 then inp else
1.21                 let
1.22 -                 val k = (Rat.neg d) * Rat.abs c / c
1.23 +                 val k = ~ d * abs c / c
1.24                   val e' = linear_cmul k e
1.25 -                 val t' = linear_cmul (Rat.abs c) t
1.26 +                 val t' = linear_cmul (abs c) t
1.27                   val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
1.28 -                 val q' = Product(Rational_lt(Rat.abs c),q)
1.29 +                 val q' = Product(Rational_lt (abs c), q)