[isabelle-dev] prems

[Makarius]

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