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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090324/a669b4c3/attachment.bin>
