[isabelle-dev] prems

[Tobias Nipkow]

Not to mention foo_tac ;-)

The English language has the term blacklist. Isar has a redlist.

Tobias

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, ...
> 
> Greetings,
> Stefan
>