[isabelle-dev] Notes on datatype_new list
jasmin.blanchette at gmail.com
Mon May 26 15:37:58 CEST 2014
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".
More information about the isabelle-dev