[isabelle-dev] Obsolete numeral experiments?

[Makarius]

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


 	Makarius