diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-17 14:45:53 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-17 14:45:53 +0000 |
| commit | 997915300fce0a4d8bf11cd1a3c9ea7762e11640 (patch) | |
| tree | 61aa89a89cb3d3056ee5c166da7cf91300439320 /coq-fontlock.el | |
| parent | fd4b0f8bdbb42fe6ca061bf94ee2a1e0a428d379 (diff) | |
Added "Induction" as tactic
Diffstat (limited to 'coq-fontlock.el')
| -rw-r--r-- | coq-fontlock.el | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index 6ac5daa6..5e9bf556 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,9 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.3 1997/10/17 14:45:53 hhg +;; Added "Induction" as tactic +;; ;; Revision 1.2 1997/10/13 17:10:29 tms ;; *** empty log message *** ;; @@ -94,6 +97,7 @@ "Exact" "Generalize" "Hnf" +"Induction" "Injection" "Intro" "Intros" |