[isabelle-dev] types and locales

[Mamoun FILALI-AMINE]

Makarius a écrit :
> On Tue, 24 Mar 2009, filali at irit.fr wrote:
>
>>  I have a problem with types and locales: in the attached file
>
>> The attached file has been processed by the Isabelle snapshot of 
>> 23-Mar-2009.
>
> Looks like their is still a problem with implicitly fixed variables in 
> locale expressions.  It appears to work if you make the binding of 
> "init" explicit in locale r1, using the 'for' in postfix notation:
>
> locale r1 =
>   r0 "init :: 'buffer => ('buffer \<times> 'value) set => 'value" for 
> init
>   + fixes d2i :: "('buffer \<times> 'buffer) => 'buffer"
> begin
>
> ...
Actually it does work now.
May be a corresponding example and syntax diagram (inline)
could help

Thanks
>
>
>     Makarius
Mamoun