[isabelle-dev] types and locales

[filali at irit.fr]

Hello,

  I have a problem with types and locales: in the attached file,I tried
to locate the problem as far as I could.
The problem is that I cannot declare a function inside a locale due to a
typing
error that I do not understand. Moreover, if in a preceding locale, I
suppress
the declaration of another function, the same function becomes well typed.
(I had a similar problem with Isabelle2008)
 The attached file has been processed by the Isabelle snapshot of
23-Mar-2009.

Thanks.

Mamoun Filali
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pb_23.thy
Type: /
Size: 2310 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090324/a669b4c3/attachment-0002.bin>