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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to