[isabelle] Question about locales
I have defined a locale
locale concept1 = fixes a b assumes ...
and another locale
locale L =
definition aa where ...
definition bb where ...
Now, aa and bb in L model concept1. However, writing
interpretation concept1[aa bb]
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 ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and