[isabelle-dev] Sort constraints syntax

Tobias Nipkow nipkow at in.tum.de
Thu Apr 19 14:16:30 CEST 2012


As I said: add them later.

Tobias

Am 19/04/2012 14:09, schrieb Makarius:
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



More information about the isabelle-dev mailing list