berghofe at in.tum.de
Wed Nov 21 18:12:03 CET 2007
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, ...
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
More information about the isabelle-dev