#544 (Feb 1, 2018, 12:50:08 AM)

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)
2. performance fine-tuning of hot spot; (detail / hgweb)
3. tuned; (detail / hgweb)
4. more efficient tokens_match_ord based on token_kind_index;
   tuned; (detail / hgweb)
5. more abstract type; (detail / hgweb)
6. tuned; (detail / hgweb)
7. clarified signature; (detail / hgweb)
8. clarified signature; (detail / hgweb)
9. explicit dummy token; (detail / hgweb)
10. clarified modules; (detail / hgweb)
11. clarified signature; (detail / hgweb)

Started by an SCM change

This run spent:

• 6 sec waiting;
• 1 hr 13 min build duration;
• 1 hr 13 min total from scheduled to completion.