Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";
Changeset 67558:c46910a6bfce by wenzelm:
proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for &quot;0 &lt;= c &amp; 0 &lt;= a ==&gt; a + bb = 1 &amp; c &lt;= 1 ==&gt; bb * c * 4 &lt;= (12::real)&quot;;
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)