Changes

Summary

1. proof of concept for algebraically founded word types
2. more lemmas
3. option to report results of solve_direct as explicit warnings
4. modernized option
5. CONTRIBUTORS
6. Probability: move some theorems from AFP/Density_Compiler
7. Probability: variant of central limit theorem with non-zero mean
8. HOL-Probability: more about probability, prepare for Markov processes in the AFP
9. Merge
10. new theorems including the theory FurtherTopology
11. clarified magic values (see also java/io/BufferedInputStream.java);
12. clarified stream operations; added XZ data compression;
13. tuned signature;
14. clarified modules; afford explicit string composition in terminate_lines;
15. more general read_stream: return actual byte count;
16. clarified modules;