[isabelle] Sublocales


I'm wondering whether it is possible to declare a sublocale when the one of
the records is an extension of the other. Suppose I first define

locale ab_locale

which is based off the record (a_object::'a, b_object::'b), and later
decide it would be useful to have a more general

locale a_locale

which is based off the record (a_object::'a). Could I make ab_object a
sublocale of a_object (here I would just want to set the a_object's equal)?


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