[isabelle-dev] Obsolete numeral experiments?

Makarius makarius at sketis.net
Wed May 29 23:33:41 CEST 2013

On Tue, 28 May 2013, Makarius wrote:

> 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.

I've done that now in 0d3165844048, after spending time beforehand to 
update it to changes in print translation interfaces.  (Just the usual 
renovation before demolition.)


More information about the isabelle-dev mailing list