src/HOL/Tools/string_syntax.ML
Mon, 30 Sep 2024 20:30:59 +0200 wenzelm clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
Sun, 01 Sep 2024 19:35:30 +0200 wenzelm proper string syntax (amending 70076ba563d2);
less more (0) -10 -2 tip