diff --git a/library/init/core.lean b/library/init/core.lean
index 13c075e03c..01a7173b3a 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -84,7 +84,6 @@ reserve infixr ` :: `:67
 
 /- Control -/
 reserve infixr ` <|> `:2
-reserve infixr `; `   :3
 reserve infixr ` >>= `:55
 reserve infixr ` >=> `:55
 reserve infixl ` <*> `:60
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index f443439955..0dcca40d40 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -89,6 +89,10 @@ def letLhsPat     := parser! termParser >> " := "
 def letLhs        := (try letLhsId <|> try letLhsBinders <|> letLhsPat)
 @[builtinTermParser] def «let» := parser! "let " >> letLhs >> termParser >> "; " >> termParser
 
+@[builtinTermParser] def not    := parser! symbol "¬" 40 >> termParser 40
+@[builtinTermParser] def bnot   := parser! symbol "!" 40 >> termParser 40
+@[builtinTermParser] def uminus := parser! "-" >> termParser 100
+
 def namedArgument  := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def app     := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
 def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
@@ -99,24 +103,50 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
 
 @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
 
+@[builtinTermParser] def prod  := tparser! infixR " × " 35
+
 @[builtinTermParser] def add   := tparser! infixL " + "  65
 @[builtinTermParser] def sub   := tparser! infixL " - "  65
 @[builtinTermParser] def mul   := tparser! infixL " * "  70
 @[builtinTermParser] def div   := tparser! infixL " / "  70
 @[builtinTermParser] def mod   := tparser! infixL " % "  70
 @[builtinTermParser] def modN  := tparser! infixL " %ₙ " 70
+@[builtinTermParser] def pow   := tparser! infixR " ^ " 80
 
 @[builtinTermParser] def le    := tparser! unicodeInfixL " ≤ " " <= " 50
 @[builtinTermParser] def ge    := tparser! unicodeInfixL " ≥ " " >= " 50
 @[builtinTermParser] def lt    := tparser! infixL " < " 50
 @[builtinTermParser] def gt    := tparser! infixL " > " 50
 @[builtinTermParser] def eq    := tparser! infixL " = " 50
+@[builtinTermParser] def ne    := tparser! infixL " ≠ " 50
 @[builtinTermParser] def beq   := tparser! infixL " == " 50
+@[builtinTermParser] def bne   := tparser! infixL " != " 50
+@[builtinTermParser] def heq   := tparser! unicodeInfixL " ≅ " " ~= " 50
+@[builtinTermParser] def equiv := tparser! infixL " ≈ " 50
+
+@[builtinTermParser] def subst := tparser! infixR " ▸ " 75
 
 @[builtinTermParser] def and   := tparser! unicodeInfixR " ∧ " " /\\ " 35
 @[builtinTermParser] def or    := tparser! unicodeInfixR " ∨ " " \\/ " 30
 @[builtinTermParser] def iff   := tparser! unicodeInfixL " ↔ " " <-> " 20
 
+@[builtinTermParser] def band  := tparser! infixL " && " 35
+@[builtinTermParser] def bor   := tparser! infixL " || " 30
+
+@[builtinTermParser] def append := tparser! infixL " ++ " 65
+@[builtinTermParser] def cons   := tparser! infixR " :: " 67
+
+@[builtinTermParser] def orelse      := tparser! infixR " <|> " 2
+@[builtinTermParser] def andthen     := tparser! infixR " >> "  60
+@[builtinTermParser] def bind        := tparser! infixR " >>= " 55
+@[builtinTermParser] def andM        := tparser! infixR " <&> " 100
+@[builtinTermParser] def seq         := tparser! infixL " <*> " 60
+@[builtinTermParser] def seqLeft     := tparser! infixL " <* "  60
+@[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
+@[builtinTermParser] def map         := tparser! infixR " <$> " 100
+@[builtinTermParser] def mapConst    := tparser! infixR " <$ "  100
+@[builtinTermParser] def mapConstRev := tparser! infixR " $> "  100
+
 end Term
 
 end Parser
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index f2395d8895..8268825c0a 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
          {"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},
          {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
-         {"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"..", 0}, {"...", 0}, {",", 0}, {"=>", 0},
+         {"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"..", 0}, {"...", 0}, {",", 0}, {";", 0}, {"=>", 0},
          {".", 0}, {":", 0}, {"!", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
          {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
          {"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec},
diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean
index 568bbcdda5..1adf1b844b 100644
--- a/tests/playground/termparsertest1.lean
+++ b/tests/playground/termparsertest1.lean
@@ -100,7 +100,10 @@ match x with
 "let x.y := f 10; x",
 "let x.1 := f 10; x",
 "let x[i].y := f 10; x",
-"let x[i] := f 20; x"
+"let x[i] := f 20; x",
+"-x + y",
+"!x",
+"¬ a ∧ b"
 ];
 testFailures [
 "f {x : a} -> b",