[isabelle-dev] prems

Tobias Nipkow 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.

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
> 



More information about the isabelle-dev mailing list