Deprecation warnings for match ⋯ with., fun., λ., and intro..

def Batteries.Tactic.matchWithDot : Lean.ParserDescr

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

def Batteries.Tactic.funDot : Lean.ParserDescr

The syntax fun. has been deprecated in favor of nofun.

def Batteries.Tactic.lambdaDot : Lean.ParserDescr

The syntax λ. has been deprecated in favor of nofun.

def Batteries.Tactic.«tacticMatch_,,With.» : Lean.ParserDescr

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

def Batteries.Tactic.introDot : Lean.ParserDescr

The syntax intro. is deprecated in favor of nofun.