[isabelle-dev] prems

[Stefan Berghofer]

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

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe