Re: [isabelle] Variables in locale assumptions
On Mon, 24 Feb 2014, Makarius wrote:
On Mon, 24 Feb 2014, Gerwin Klein wrote:
or if you need to constrain types?
The 'constrains' element is easier to get rid of. I would like to see
some constructive proofs where you "need to constrain types", as you
say. This is usually just a workaround to specify locale type arguments,
but if that would be supported directly, the need would go away.
Maybe you have actually missed the important locale expression
improvements by Clemens Ballarin from Isabelle2009. See the NEWS, e.g.
- In locale expressions, instantiation replaces renaming. Parameters
must be declared in a for clause. To aid compatibility with previous
parameter inheritance, in locale declarations, parameters that are not
'touched' (instantiation position "_" or omitted) are implicitly added
with their syntax at the beginning of the for clause.
In most situations a locale expression suffix "for x :: T" can be used to
instantiate types in imports. I had cleaned up AFP in this respect
already some years ago, but in various newer entries old 'constrains'
seem to have come back. Time for spring cleaning?
This archive was generated by a fusion of
Pipermail (Mailman edition) and