[isabelle-dev] Obsolete numeral experiments?

Makarius makarius at sketis.net
Tue May 28 15:53:36 CEST 2013

What is the status of the following experiments wrt. the regular numerals 
in main HOL?


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?


More information about the isabelle-dev mailing list