[isabelle-dev] types and locales

filali at irit.fr filali at irit.fr
Tue Mar 24 22:25:08 CET 2009


  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
error that I do not understand. Moreover, if in a preceding locale, I
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


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>

More information about the isabelle-dev mailing list