Changes

Summary

1. merge
2. use alternative version of COMB
3. adaptation for current isabelle development version
4. getting rid of superfluous proofs skript
5. get rid of smt
6. getting rid of a smt command
7. finishing TS proofs for COMB integration
8. working on rework to conform COMB's proof
9. finished rework for COMB
10. added projection to the distribution of one part of the sum type
11. alternative proof for COMB, needed some rework in bit ts and opt
12. Sum_Distribution, a formalization of a Distribution over a Sum type
13. added an abbreviation for readability in BIT_2comp_on2
14. tidy up BIT_2comp_on2
15. getting rid of smt
16. finished rework of BIT on 2
17. finished rework phase A of BIT
18. reworking BIT 2comp on2 proofs, done: bit_yx'
19. more tidy up in TS
20. tidy up
21. used Phase_Partitioning thm in TS
22. refactoring TS
23. bringing TS proof into invariant form
24. more simplification of BIT's proof
25. simplifying proof of BIT being 1.75-competitive