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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and