On Wed, 21 Nov 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.
Note that "prems" is a special name just like "this"; the system does not
stop users to redefine such names, but this will result in unecessary
confusion.
Concerning the special meaning of "prems" as the list of *all* premises of
the current context: this feature was found to result in unstructured
proofs, i.e. it has been moved to the category of ``improper'' language
elements (like foo_tac and commands 'apply' and 'done').
Concerning improper Isar language elements in general: Isar has been
traditionally very liberal in admitting language elements that are outside
the scope of proper structured proof composition. This has been so
successful that the traditional tactical style has been assimilated
completely and tactic-only users have even discontinued the classical
interaction mode of Isabelle in favour of the Isar infrastructure.
In Proof General, improper elements are marked up uniformly using
font-lock-reference-face, which happens to default to red in XEmacs, but
something else in GNU Emacs. In any case, you are free to redefine the
face in any way you like, e.g. using the "Edit Faces" menu.
Makarius
