[isabelle-dev] Notes on datatype_new list

[Jasmin Blanchette]

Am 26.05.2014 um 15:24 schrieb Makarius <makarius at sketis.net>:

> I think you could afford an actual keyword for the "dead" modifier and use it without colon, like "lazy" in HOLCF/domain.  That would substract "dead" from the normal identifier space, but merely means its very few occurrences on AFP/Jinja and AFP/JinjaThreads need to be quoted.

Indeed, that would make sense. And perhaps we don't even need to make it a keyword? It shouldn't be hard to parse "(dead 'a)" with "Parse.reserved" for "dead".

Jasmin