thys/BitCoded2CT.thy
2019-09-12 Chengsong proof attempt
less more (0) tip