[isabelle-dev] Obsolete numeral experiments?

[Makarius]

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