diff options
Diffstat (limited to 'lego/lego.el')
| -rw-r--r-- | lego/lego.el | 21 |
1 files changed, 3 insertions, 18 deletions
diff --git a/lego/lego.el b/lego/lego.el index 24e1a63e..26b869cb 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -277,20 +277,9 @@ Given is the first SPAN which needs to be undone." ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun lego-intros () - "intros." - (interactive) - (insert "intros ")) - -(defun lego-Intros () - "insert Intros." - (interactive) - (insert "Intros ")) - -(defun lego-Refine () - "Insert Refine." - (interactive) - (insert "Refine ")) +(proof-defshortcut lego-Intros "Intros " ?I) +(proof-defshortcut lego-intros "intros " ?i) +(proof-defshortcut lego-Refine "Refine " ?r) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Lego Indentation ;; @@ -397,10 +386,6 @@ Checks the width in the `proof-goals-buffer'" (proof-config-done) - (define-key (current-local-map) [(control c) ?i] 'lego-intros) - (define-key (current-local-map) [(control c) ?I] 'lego-Intros) - (define-key (current-local-map) [(control c) ?r] 'lego-Refine) - ;; outline (make-local-variable 'outline-regexp) |