[isabelle-dev] Sort constraints syntax

Makarius makarius at sketis.net
Thu Apr 19 14:09:59 CEST 2012


On Thu, 19 Apr 2012, Tobias Nipkow wrote:

> I did not propose to add this before the release, but I don't see any 
> harm in discussing it now. In fact, now people may be more alert than 
> later. Of course you are welcome to add your two cents later.

I do see a harm.  A release is not a trivial thing, and one needs to 
concentrate on solving pending problems, not posing new issues.

Concerning sort or type constraints in general: it is one of my core areas 
of resposibilities, and I don't have time to consider any changes there 
right now.


 	Makarius



More information about the isabelle-dev mailing list