[isabelle-dev] types and locales

[Makarius]

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

...


 	Makarius