Topic: localized notation
Jesse Michael Han (Jul 25 2019 at 15:16):
@Floris van Doorn what are the differences between the
localized keywords? is the main feature being able to re-introduce
localized things into the environment of a separate section?
Rob Lewis (Jul 25 2019 at 15:23):
Yes, that's the idea.
localized basically stores local notation and attribute commands, and gives a convenient way to replay these commands.
Kevin Buzzard (Jul 25 2019 at 20:07):
localized documented? I've never heard of it
Jesse Michael Han (Jul 25 2019 at 20:46):
it's at the bottom of tactics.md
Keeley Hoek (Jul 26 2019 at 02:38):
I just had the thought that perhaps Simon's "open all the parser namespaces" tactic could be unified into
Last updated: May 12 2021 at 22:15 UTC