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