## Stream: general

### Topic: localized notation

#### Jesse Michael Han (Jul 25 2019 at 15:16):

@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 (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):

Where is 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 localized

Last updated: May 12 2021 at 22:15 UTC