[isabelle] Question about locales



Hi all,

I have defined a locale

locale concept1 = fixes a b assumes ...


and another locale

locale L =
 fixes x
begin
 definition aa where ...
 definition bb where ...
end

Now, aa and bb in L model concept1. However, writing

context L
begin
 interpretation concept1[aa bb]
end

does not work. Neither does:
 interpretation L \<subseteq> concept1[aa bb]
the latter one does not bind the aa and bb to their definitions in L, but introduces them as fresh variables.

How can I achieve to make available all stuff proven in concept1 in locale L for aa and bb ?

Regards,
 Peter











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