On Tue, 28 May 2013, Brian Huffman wrote: > As for Binary.thy, I believe that all the main ideas there have already > been incorporated into the HOL numerals library, so there's no reason > not to delete it. OK, so I will delete just my old experiment Binary.thy. Makarius