Re: [isabelle] relating 2 theories



On 15 Sep 2008, at 1:22, Jeremy Dawson wrote:

Then, in a supertheory which sees both type class definitions, it is possible to express and prove that one type class is a subclass of the other (by the <-form of the instance command). Unfortunately it is not possible to express (except, I guess, in two independent theories) that type class a < type class b, and vice versa - understandably, Isabelle doesn't like cyclic subclass relationships.

In contrast, locales permit cyclic relationships. That is, if two locales have equivalent specifications and the parameters are the same (up to renaming) you can declare them to interpret each other.

Clemens





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