Re: [isabelle] malformed dependency





In order to circumvent this problem, you can use together with defs(unchecked) my package for checking overloaded definitions. It is more powerful than the built-in test of Isabelle and might be able to prove the consistency of your definitions (and it also tells you when your definitions are definitely circular and such). You can find it at http://www4.in.tum.de/~obua/checkdefs. Don't hesitate to ask me if you have more questions,

There is now a new version of the mentioned package available that works together with the latest Isabelle repository version. It proves that your definitions in theory PM are OK.

Steven





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.