diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index c78b4c573..0cd69dde3 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -11,7 +11,7 @@
   '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
-    "print" "theorem" "example" "abbreviation" "abstract"
+    "print" "theorem" "proposition" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 460eaf126..3c386217c 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -127,7 +127,7 @@ void init_token_table(token_table & t) {
          {g_qed_unicode, "qed"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
-        {{"lemma", "theorem"}, {"premise", "variable"}, {"premises", "variables"},
+        {{"lemma", "theorem"}, {"proposition", "theorem"}, {"premise", "variable"}, {"premises", "variables"},
          {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
          {"record", "structure"}, {nullptr, nullptr}};
 
diff --git a/tests/lean/run/proposition.lean b/tests/lean/run/proposition.lean
new file mode 100644
index 000000000..eccfdda0e
--- /dev/null
+++ b/tests/lean/run/proposition.lean
@@ -0,0 +1,4 @@
+proposition tst {a b : Prop} : a → b → a ∧ b :=
+begin
+  intros, split, repeat assumption
+end