| Wed, 31 Jan 2018 21:05:47 +0100 | wenzelm | 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 | files |
| Wed, 31 Jan 2018 14:20:39 +0100 | wenzelm | performance fine-tuning of hot spot; | changeset | files |
| Wed, 31 Jan 2018 14:11:57 +0100 | wenzelm | tuned; | changeset | files |