diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 00469e84d1..89fe0980e4 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -77,6 +77,12 @@ def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> (("`(" >> ca
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
 @[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail
 
+@[builtinCommandParser] def «elab_rules» := parser! "elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts
+def elabHead := macroHead
+def elabArg  := macroArg
+def elabTail := try (" : " >> ident) >> darrow >> termParser
+@[builtinCommandParser] def «elab»       := parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail
+
 end Command
 
 end Parser