wenzelm [Thu, 18 May 2023 15:34:01 +0200] rev 78071
clarified data: avoid pointless Morphism.transform;
wenzelm [Thu, 18 May 2023 14:06:35 +0200] rev 78070
proper Token.Declaration for internal_declaration;
wenzelm [Tue, 16 May 2023 20:26:09 +0200] rev 78069
more standard treatment of morphism context;
wenzelm [Tue, 16 May 2023 19:52:50 +0200] rev 78068
tuned: avoid duplication;
wenzelm [Tue, 16 May 2023 19:43:42 +0200] rev 78067
more standard treatment of morphism context, but hardly relevant here;
wenzelm [Tue, 16 May 2023 19:42:19 +0200] rev 78066
tuned;
wenzelm [Tue, 16 May 2023 19:20:18 +0200] rev 78065
more careful treatment of set_context / reset_context for persistent morphisms;
avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition;
wenzelm [Tue, 16 May 2023 17:08:31 +0200] rev 78064
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
clarified signature;
wenzelm [Tue, 16 May 2023 15:15:56 +0200] rev 78063
tuned signature;
wenzelm [Tue, 16 May 2023 14:30:32 +0200] rev 78062
support for context within morphism (for background theory);