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

[Lawrence Paulson]

The situation involving ZF can go either way, as there are hardly any users.

How are negative integers written in ZF now? Can one still write #-3 or is it $- #3?

Larry

On 21 Sep 2014, at 16:04, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> 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
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev