Mon, 30 Sep 2024 20:30:59 +0200 clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
wenzelm [Mon, 30 Sep 2024 20:30:59 +0200] rev 81019
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
Mon, 30 Sep 2024 13:00:42 +0200 less markup: prefer "notatation" over "entity";
wenzelm [Mon, 30 Sep 2024 13:00:42 +0200] rev 81018
less markup: prefer "notatation" over "entity";
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 tip