What is the status of the following experiments wrt. the regular numerals
in main HOL?
http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Binary.thy
http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Numeral_Representation.thy
Can we delete that, and keep the history inside the history? Or are there
remaining aspects that are not in the official numeral implementation (and
reform) by Brian Huffman?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
