| Sat, 03 Feb 2018 13:54:04 +0100 |
wenzelm |
clarified overall range: include delimiters;
|
changeset |
files
|
| Fri, 02 Feb 2018 11:47:13 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Thu, 01 Feb 2018 20:29:53 +0100 |
wenzelm |
tuned: more standard use of order;
|
changeset |
files
|
| Thu, 01 Feb 2018 17:27:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Feb 2018 17:21:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Feb 2018 17:15:07 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 01 Feb 2018 15:31:25 +0100 |
wenzelm |
clarified signature: prefer proper order operation;
|
changeset |
files
|
| Thu, 01 Feb 2018 15:12:57 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 01 Feb 2018 13:55:10 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| 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
|