#1445 (Jan 31, 2018, 9:40:02 PM)

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)"; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 0 sec waiting;
• 1 hr 16 min build duration;
• 1 hr 21 min total from scheduled to completion.