Am 26.05.2014 um 15:24 schrieb Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
