diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index be223582f4..dd16d5f906 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -12,11 +12,11 @@ import Init.Prelude
 
 namespace Lean.Parser.Syntax
 
-syntax:65 [addPrec] prec " + " prec:66 : prec
-syntax:65 [subPrec] prec " - " prec:66 : prec
+syntax:65 (name := addPrec) prec " + " prec:66 : prec
+syntax:65 (name := subPrec) prec " - " prec:66 : prec
 
-syntax:65 [addPrio] prio " + " prio:66 : prio
-syntax:65 [subPrio] prio " - " prio:66 : prio
+syntax:65 (name := addPrio) prio " + " prio:66 : prio
+syntax:65 (name := subPrio) prio " - " prio:66 : prio
 
 end Lean.Parser.Syntax
 
@@ -54,7 +54,7 @@ macro:max x:stx ",+,?" : stx => `(stx| sepBy1($x, ",", ", ", allowTrailingSep))
 
 macro "!" x:stx : stx => `(stx| notFollowedBy($x))
 
-syntax[rawNatLit] "natLit! " num : term
+syntax (name := rawNatLit) "natLit! " num : term
 
 infixr:90 " ∘ "  => Function.comp
 infixr:35 " × "  => Prod
@@ -160,28 +160,28 @@ macro_rules
 
 namespace Parser.Tactic
 
-syntax[intro] "intro " notFollowedBy("|") (colGt term:max)* : tactic
-syntax[intros] "intros " (colGt (ident <|> "_"))* : tactic
-syntax[revert] "revert " (colGt ident)+ : tactic
-syntax[clear] "clear " (colGt ident)+ : tactic
-syntax[subst] "subst " (colGt ident)+ : tactic
-syntax[assumption] "assumption" : tactic
-syntax[apply] "apply " term : tactic
-syntax[exact] "exact " term : tactic
-syntax[refine] "refine " term : tactic
-syntax[refine!] "refine! " term : tactic
-syntax[case] "case " ident " => " tacticSeq : tactic
-syntax[allGoals] "allGoals " tacticSeq : tactic
-syntax[focus] "focus " tacticSeq : tactic
-syntax[skip] "skip" : tactic
-syntax[done] "done" : tactic
-syntax[traceState] "traceState" : tactic
-syntax[failIfSuccess] "failIfSuccess " tacticSeq : tactic
-syntax[generalize] "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
-syntax[paren] "(" tacticSeq ")" : tactic
-syntax[withReducible] "withReducible " tacticSeq : tactic
-syntax[withReducibleAndInstances] "withReducibleAndInstances " tacticSeq : tactic
-syntax:2[orelse] tactic "<|>" tactic:1 : tactic
+syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
+syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic
+syntax (name := revert) "revert " (colGt ident)+ : tactic
+syntax (name := clear) "clear " (colGt ident)+ : tactic
+syntax (name := subst) "subst " (colGt ident)+ : tactic
+syntax (name := assumption) "assumption" : tactic
+syntax (name := apply) "apply " term : tactic
+syntax (name := exact) "exact " term : tactic
+syntax (name := refine) "refine " term : tactic
+syntax (name := refine!) "refine! " term : tactic
+syntax (name := case) "case " ident " => " tacticSeq : tactic
+syntax (name := allGoals) "allGoals " tacticSeq : tactic
+syntax (name := focus) "focus " tacticSeq : tactic
+syntax (name := skip) "skip" : tactic
+syntax (name := done) "done" : tactic
+syntax (name := traceState) "traceState" : tactic
+syntax (name := failIfSuccess) "failIfSuccess " tacticSeq : tactic
+syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
+syntax (name := paren) "(" tacticSeq ")" : tactic
+syntax (name := withReducible) "withReducible " tacticSeq : tactic
+syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
+syntax:2 (name := orelse) tactic "<|>" tactic:1 : tactic
 macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
 
 
@@ -194,21 +194,21 @@ syntax locationTarget   := "⊢" <|> "|-"
 syntax locationHyp      := (colGt ident)+
 syntax location         := withPosition("at " locationWildcard <|> locationTarget <|> locationHyp)
 
-syntax[change] "change " term (location)? : tactic
-syntax[changeWith] "change " term " with " term (location)? : tactic
+syntax (name := change) "change " term (location)? : tactic
+syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
 syntax rwRule    := ("←" <|> "<-")? term
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
-syntax[rewrite] "rewrite " rwRule (location)? : tactic
-syntax[rewriteSeq, high] "rewrite " rwRuleSeq (location)? : tactic
-syntax[erewrite] "erewrite " rwRule (location)? : tactic
-syntax[erewriteSeq, high] "erewrite " rwRuleSeq (location)? : tactic
+syntax (name := rewrite) "rewrite " rwRule (location)? : tactic
+syntax (name := rewriteSeq) (priority := high) "rewrite " rwRuleSeq (location)? : tactic
+syntax (name := erewrite) "erewrite " rwRule (location)? : tactic
+syntax (name := erewriteSeq) (priority := high) "erewrite " rwRuleSeq (location)? : tactic
 
-syntax[rw] "rw " rwRule (location)? : tactic
-syntax[rwSeq, high] "rw " rwRuleSeq (location)? : tactic
-syntax[erw] "erw " rwRule (location)? : tactic
-syntax[erwSeq, high] "erw " rwRuleSeq (location)? : tactic
+syntax (name := rw) "rw " rwRule (location)? : tactic
+syntax (name := rwSeq) (priority := high) "rw " rwRuleSeq (location)? : tactic
+syntax (name := erw) "erw " rwRule (location)? : tactic
+syntax (name := erwSeq) (priority := high) "erw " rwRuleSeq (location)? : tactic
 
 private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
   `(tactic| $tac; try (withReducible rfl))
@@ -229,31 +229,31 @@ def expandERw : Macro :=
 def expandERwSeq : Macro :=
   fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
 
-syntax[injection] "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
+syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
-syntax[«have»] "have " haveDecl : tactic
-syntax[«suffices»] "suffices " sufficesDecl : tactic
-syntax[«show»] "show " term : tactic
-syntax[«let»] "let " letDecl : tactic
-syntax[«let!»] "let! " letDecl : tactic
-syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
+syntax (name := «have») "have " haveDecl : tactic
+syntax (name := «suffices») "suffices " sufficesDecl : tactic
+syntax (name := «show») "show " term : tactic
+syntax (name := «let») "let " letDecl : tactic
+syntax (name := «let!») "let! " letDecl : tactic
+syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 
 syntax inductionAlt  := "| " (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " withPosition( (colGe inductionAlt)+)
-syntax[induction] "induction " term,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
+syntax (name := induction) "induction " term,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
 syntax casesTarget := atomic(ident " : ")? term
-syntax[cases] "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
+syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
 
 syntax matchAlt  := "| " term,+ " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax matchAlts := withPosition((colGe matchAlt)+)
-syntax[«match»] "match " matchDiscr,+ (" : " term)? " with " matchAlts : tactic
+syntax (name := «match») "match " matchDiscr,+ (" : " term)? " with " matchAlts : tactic
 
-syntax[introMatch] "intro " matchAlts : tactic
+syntax (name := introMatch) "intro " matchAlts : tactic
 
-syntax[existsIntro] "exists " term : tactic
+syntax (name := existsIntro) "exists " term : tactic
 
 /- We use a priority > default, to avoid ambiguity with the builtin `have` notation -/
-macro[high] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
 
 syntax "repeat " tacticSeq : tactic
 macro_rules