localized notation

Stream: general

[Jesse Michael Han]

@Floris van Doorn what are the differences between the local and localized keywords? is the main feature being able to re-introduce localized things into the environment of a separate section?

[Rob Lewis]

Yes, that's the idea. localized basically stores local notation and attribute commands, and gives a convenient way to replay these commands.

[Kevin Buzzard]

Where is localized documented? I've never heard of it

[Jesse Michael Han]

it's at the bottom of tactics.md

[Keeley Hoek]

I just had the thought that perhaps Simon's "open all the parser namespaces" tactic could be unified into localized