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

[Florian Haftmann]

After realising that HOL and ZF numerals are already separate lexical
categories (though the history of this being so ist not clear to me at
the moment), I finally took the adventure of turning HOL numerals into
unsigned numerals also lexically (logically, this has already been the
case for a long time). See now 6d46ad54a2ab.
	
Two issues remain left to settle on.
	
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.

Awaiting your suggestions and advice,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140921/03894060/attachment.asc>