Update manual with PR instructions for abbreviations

[kckennylau]

Added instructions for modifying abbreviation identifiers.

[kim-em]

Could you modify the text here to request discussing on Zulip first? I don't want to encourage people who don't know what they're doing to spam PRs that require Marc's review.

[mhuisi]

The user manual is not the right place for instructions on the development workflow of contributing to vscode-lean4. docs/dev.md is a better place for this kind of information.

Ideally, this guide should also document potential caveats of adding new abbreviations:

• For any new abbreviation, it must be confirmed that for all abbreviations that are strict prefixes of the new abbreviation and which are currently no strict prefix of another abbreviation, the loss of eager abbreviation replacement of the prefix abbreviation is acceptable.
• For any new abbreviation that contains brackets from autoClosingPairs in vscode-lean4/language-configuration.json, the closing bracket that is inserted automatically by VS Code should not skip over any other abbreviation, e.g. by eagerly replacing an abbreviation too early due to the inserted bracket, or because there are abbreviations that contain the opening bracket, but do not contain the closing bracket at all.
• When adding abbreviations or changing the relative order of abbreviations, if any of the affected abbreviations shares a non-empty prefix with another abbreviation and both abbreviations are also the shortest abbreviations that start with this prefix, then it must be ensured that the abbreviation that should be used when triggering abbreviation replacement on the prefix comes first in the relative order.