Lukas Stevens (Jul 14 2021 at 09:17): Lukas Stevens (Jul 14 2021 at 09:17):Why is ' classified as a special character in string_syntax.ML and therefore not printed as e.g. STR ''won't''?
Simon Wimmer (Sep 21 2021 at 16:47):It has a special meaning as an escape character when you define user-space syntax but I have no idea whether that is related.
Last updated: Nov 07 2025 at 16:23 UTC