[isabelle-dev] NEWS: Lexically unsigned numerals for HOL

[Makarius]

On Sun, 21 Sep 2014, Florian Haftmann wrote:

> a) Currently, the prefix for (signed!) ZF numerals is »#«. Since
> operations for integers in ZF are mainly associated with »$« (e.g., »_
> $+ _«,  »_ $* _«), maybe it would be more consistent to prefer »$« also
> here. As far as I understand from the sources, ZF numerals are not
> polymorphic but restricted to set int in ZF.
>
> b) The lexical category for signed numerals is named »xnum«. Maybe
> »signed_num« would be more explicit.

The "x" in "xnum" can be explained historically as a special marker for
something that is a numeral with some extra decoration.  The signed vs. 
unsigned aspect came much later, and was not there in distant past.

Looking once again at ZF xnum syntax, I think it can be expressed without 
the xnum token, and without any syntax change for now -- that may be 
reconsidered independently.

I have presently something that might soon become a changeset to remove 
the xnum token syntax from Pure.


 	Makarius