Thu, 18 May 2023 23:21:05 +0200 tuned;
wenzelm [Thu, 18 May 2023 23:21:05 +0200] rev 78074
tuned;
Thu, 18 May 2023 23:20:41 +0200 tuned;
wenzelm [Thu, 18 May 2023 23:20:41 +0200] rev 78073
tuned;
Thu, 18 May 2023 17:21:29 +0200 clarified signature: more explicit types;
wenzelm [Thu, 18 May 2023 17:21:29 +0200] rev 78072
clarified signature: more explicit types;
Thu, 18 May 2023 15:34:01 +0200 clarified data: avoid pointless Morphism.transform;
wenzelm [Thu, 18 May 2023 15:34:01 +0200] rev 78071
clarified data: avoid pointless Morphism.transform;
Thu, 18 May 2023 14:06:35 +0200 proper Token.Declaration for internal_declaration;
wenzelm [Thu, 18 May 2023 14:06:35 +0200] rev 78070
proper Token.Declaration for internal_declaration;
Tue, 16 May 2023 20:26:09 +0200 more standard treatment of morphism context;
wenzelm [Tue, 16 May 2023 20:26:09 +0200] rev 78069
more standard treatment of morphism context;
Tue, 16 May 2023 19:52:50 +0200 tuned: avoid duplication;
wenzelm [Tue, 16 May 2023 19:52:50 +0200] rev 78068
tuned: avoid duplication;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 tip