nipkow at in.tum.de
Wed Nov 21 18:16:14 CET 2007
Not to mention foo_tac ;-)
The English language has the term blacklist. Isar has a redlist.
Stefan Berghofer wrote:
> Clemens Ballarin wrote:
>> The new PG seems to colour the word "prems" red wherever it occurs.
>> I think this is overdoing it a bit: prems is just a name and doesn't
>> belong to a syntactic category (correct me if I'm wrong). Users
>> might introduce this name and rightfully use it.
> By the way, a similar effect occurs with names such as goal1, goal2, ...
More information about the isabelle-dev