diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-02 12:05:41 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-02 12:05:41 +0000 |
| commit | e6d5b8b8b19ae60f76f34563b0a8eca4fb89e6e2 (patch) | |
| tree | c067a35ef2d1b8d5f57162e9f621fbd40a3fbfd7 /lego | |
| parent | dc7af5fb2c02eb960815e01741b9d2cb59c3844e (diff) | |
Added proof-assistant-keymap and commands for defining insert keys.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/example.l | 1 | ||||
| -rw-r--r-- | lego/lego.el | 21 |
2 files changed, 3 insertions, 19 deletions
diff --git a/lego/example.l b/lego/example.l index 535d5712..525db25b 100644 --- a/lego/example.l +++ b/lego/example.l @@ -5,7 +5,6 @@ *) Module example Import lib_logic; - Goal {A,B:Prop}(A /\ B) -> (B /\ A); intros; Refine H; 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) |