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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
