diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 043e5bc5a3..bdd9e473fd 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -10,7 +10,8 @@
 (defconst lean-keywords
   '("import" "prelude" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
-    "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "example" "abbreviation"
+    "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
+    "print" "theorem" "example" "abbreviation"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 15aedb9871..7939da1adc 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -102,7 +102,8 @@ void init_token_table(token_table & t) {
          {g_qed_unicode, "qed"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
-        {{"lemma", "theorem"}, {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
+        {{"lemma", "theorem"}, {"premise", "variable"}, {"premises", "variables"},
+         {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
          {"record", "structure"}, {nullptr, nullptr}};
 
     auto it = builtin;
diff --git a/tests/lean/run/premises.lean b/tests/lean/run/premises.lean
new file mode 100644
index 0000000000..76b63046cf
--- /dev/null
+++ b/tests/lean/run/premises.lean
@@ -0,0 +1,9 @@
+variable a : Prop
+variables b c : Prop
+premise  Ha : a
+premises (Hb : b) (Hc : c)
+
+theorem tst : a ∧ b ∧ c :=
+and.intro Ha (and.intro Hb Hc)
+
+check tst