a general mechanism for mixins

[kohlhase]

We need a general mechanism that allows to mix in (i.e. probably provide the necessary symbols and semantic macros) flexiformalizations that are connected via a view.

[Jazzpirate]

This also entails a mechanism in particular for conservative extensions of mathstructures (an instance should automatically be an instance of all conservative extensions, ideally without syntactic overhead), which will also require a corresponding mechanism in MMT (to some degree - this is partially subsumed by manifest fields in record types, if a record's type is inferred/asserted adequately)