Changes

Summary

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