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