diff -r 222333d2bdc2 -r 43b87bab0dac thys2/SizeBound6CT.thy