Summary
- merge
- use alternative version of COMB
- adaptation for current isabelle development version
- getting rid of superfluous proofs skript
- get rid of smt
- getting rid of a smt command
- finishing TS proofs for COMB integration
- working on rework to conform COMB's proof
- finished rework for COMB
- added projection to the distribution of one part of the sum type
- alternative proof for COMB, needed some rework in bit ts and opt
- Sum_Distribution, a formalization of a Distribution over a Sum type
- added an abbreviation for readability in BIT_2comp_on2
- tidy up BIT_2comp_on2
- getting rid of smt
- finished rework of BIT on 2
- finished rework phase A of BIT
- reworking BIT 2comp on2 proofs, done: bit_yx'
- more tidy up in TS
- tidy up
- used Phase_Partitioning thm in TS
- refactoring TS
- bringing TS proof into invariant form
- more simplification of BIT's proof
- simplifying proof of BIT being 1.75-competitive