more standard treatment of morphism context, but hardly relevant here;

tuned;

more careful treatment of set_context / reset_context for persistent morphisms; avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition;

clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context; clarified signature;

tuned signature;

support for context within morphism (for background theory);

proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";

clarified signature;

tuned;

tuned;