doc: also mention the full syntax for the deprecated attribute

The other day, I wanted to apply the full form (i.e., with both a custom
message and a deprecation date) in mathlib and failed to guess the correct
order of these two. The attribute doc-string seemed to suggest that combining
them was impossible (which was luckily false).

To prevent this from re-occurring, clarify the doc-string by
- mentioning that a custom message and deprecation date can be combined
- what the expected order of these two is

Author: grunweg

src/Init/Notation.lean

@@ -564,6 +564,9 @@ existing code. It may be removed in a future version of the library.
 * `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
 * `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
 * `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
+* the last two options can be combined:
+  `@[deprecated myBetterDef "use myBetterDef instead" (since := "2024-04-21")]`
+  customizes the deprecation message and specifies the deprecation date
 -/
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr