diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index eadd7f338..53607ac7f 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -201,7 +201,7 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
            (λ Hbt : b = true,  false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf))
            (λ Hbf : b = false, trans Haf (symm Hbf)))
 
-theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
+theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b
 := boolext Hab Hba
 
 theorem eqt_intro {a : Bool} (H : a) : a = true
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 48637ac5f..81c51c872 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -28,7 +28,7 @@
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|in\\|let\\|forall\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)
-    ("\\(->\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-⟷]\\)" . 'font-lock-constant-face)
+    ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
     ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)
     ("\\_<\\(\\b.*_tac\\|Cond\\|OrElse\\|T\\(?:hen\\|ry\\)\\|When\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face)
     ("\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|builtin\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))