#989 (Aug 18, 2019, 12:50:10 AM)

1. clarified signature; (detail / hgweb)
2. discontinued peek_status: unused and not clearly defined; (detail / hgweb)
3. more documentation on oracles; (detail / hgweb)
4. proper theory context for global props; (detail / hgweb)
5. more thorough check, using full dependency graph of finished proofs; (detail / hgweb)
6. added ML antiquotation @{oracle_name}; (detail / hgweb)
7. more robust, notably for open_proof of unnamed derivation; (detail / hgweb)
8. tuned comments; (detail / hgweb)
9. NEWS; (detail / hgweb)
10. more accurate proposition for cheat_tac (command 'sorry'); (detail / hgweb)
11. added command 'thm_oracles'; (detail / hgweb)
12. clarified type for recorded oracles; (detail / hgweb)
13. unused; (detail / hgweb)
14. clarified signature; (detail / hgweb)
15. clarified modules; (detail / hgweb)
16. clarified lookup operations: more scalable for multiple retrieval; (detail / hgweb)
17. clarified signature; (detail / hgweb)

Started by an SCM change

This run spent:

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