[isabelle-dev] Obsolete numeral experiments?
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