Changes

Summary

1. superseded by plain_identify;
2. tolerate odd negative times from old log files (before 1698e9ccef2d);
3. prefer main entry points of HOL;
4. tuned signature;
5. clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
6. more robust sorted_entries;
7. more convenient build_log_history;
8. tuned;
9. more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
10. polyml-test version based on experimental branch NewTestRegisterSave;