[isabelle-dev] Notes on datatype_new list

[Makarius]

On Mon, 26 May 2014, Dmitriy Traytel wrote:

>>  Just on the squiggles in isolation: if these are rare add-on options one
>>  could invent long / explicit keywords for them (or Parse.literal items).
>
> grep gives 371 occurences of "-:" in IsaFoR's development repository. So 
> it's not a rare add-on, but an important performance optimization.

If it is only an optimization it is conceptually still "rare". But of 
course it is also possible to invent short keywords -- after some 
empricial studies about the danger of clashing with common identifiers.

The datatypes manual calls the above "dead" so that is an obvious choice 
to try out.


The BNF package has a slight tendency to cryptic shortcuts to conceal it 
from outsiders (like category theory in general).


 	Makarius