Re: [isabelle] Specializing types in locales



Dear Clemens,

The constrains element stems from times when locale expressions were based on renaming rather than instantiation. It is deprecated and will disappear in a future release of Isabelle.

When it disappears, please provide a way to simulate the behaviour of constrains. I use it a lot to undo the havoc that locale inheritance causes on type variable names. It is no use to have ten type variables 'a to 'j floating around that get renamed every now and then. Your approach with for would work nicely if it did not erase all mixfix syntax annotations on the parameters. It is hard to consistently change mixfix syntax when it is repeated all over the place.

Andreas






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