Changes

Summary

1. proper theory for export_proofs;
2. tuned signature;
3. merged
4. just tidied one proof
5. proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);
6. oops — fixed symbols!!
7. reorganisation to eliminate Brouwer_Fixpoint from complex analysis
8. merged
9. Inverse function theorem + lemmas
10. back to more elementary Buffer.T -- less intermediate garbage;
11. unused;
12. unused;
13. more direct output of XML material -- bypass Buffer.T;
14. clarified signature;
15. tuned;
16. more direct output of XML material -- bypass Buffer.T;
17. more scalable protocol_message: use XML.body directly (Output.output hook is not required);
18. clarified signature;
19. tuned;