Re: [isabelle] Variables in locale assumptions

On Fri, 21 Feb 2014, Stephan van Staden wrote:

It's this type constraint that surprised me. The post by Makarius explains it, but as a user I would prefer to have complete separation. Is there a compelling reason why it's implemented as it is?

Feasibility and complexity of implementation. In order to move locales once again some steps forward, one should probably give up rarely used old features like 'defines' and 'constrains' (which have heavy weight and little real applications).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.