[isabelle-dev] types and locales
makarius at sketis.net
Wed Mar 25 00:17:49 CET 2009
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
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"
More information about the isabelle-dev