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