From 4bee7554a3babcfa4e0bb021f7face42744a299a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Nov 2014 14:50:10 -0800 Subject: [PATCH] chore(lean-mode): remove 'annoying' abbreviations --- src/emacs/lean-mode.el | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 62d115e8f..09ff58ce2 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -96,10 +96,7 @@ (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)) (define-abbrev-table 'lean-abbrev-table - '(("var" "variable") - ("vars" "variables") - ("def" "definition") - ("th" "theorem"))) + '()) (defvar lean-mode-map (make-sparse-keymap) "Keymap used in Lean mode")