Re: [isabelle] type variable and locales extension
On 02/10/2014 02:00 PM, Henri Debrat wrote:
locale M2 = M1 +
I guess that without having any assumptions over "getval" and "setval"
connecting the both, what you experience might be the expected result.
To give such a connection explicitly, you can use:
locale M2 =
M1 getval for getval :: "'msg => 'val" +
fixes setval :: "'val => 'msg"
This archive was generated by a fusion of
Pipermail (Mailman edition) and