[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