diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index f21878b8f..1e0843a34 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -194,6 +194,10 @@ order for the change to take effect."
 (defcustom lean-input-translations
   (let ((max-lisp-eval-depth 2800)) `(
 
+  ;; Negation
+
+  ("not" . ("¬"))
+
   ;; Equality and similar symbols.
 
   ("eq"  . ,(lean-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))
@@ -378,7 +382,7 @@ order for the change to take effect."
   ("join"     . ,(lean-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))
 
   ;; Arrows.
-
+  ("iff" . ("↔"))
   ("l"  . ,(lean-input-to-string-list "λ←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹     ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲                                     "))
   ("r"  . ,(lean-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴    ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸"))
   ("u"  . ,(lean-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                           "))