blob: bbfaae429c114264262e1e751b581110e9fd9c95 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
;; default abbrev table
(define-abbrev-table 'coq-mode-abbrev-table
'(
("u" "unfold" nil 0)
("si" "simpl" nil 0)
("t" "trivial" nil 0)
("dec" "decompose []" nil 0)
("ab" "absurd" nil 0)
("ao" "abstract omega" nil 0)
("s" "simpl" nil 0)
("r<" "rewrite <-" nil 0)
("r" "rewrite" nil 0)
("di" "discriminate" nil 0)
("p" "Print" nil 0)
("indv" "Inductive" nil 0)
("o" "abstract omega" nil 0)
("l" "Lemma :" nil 0)
("de" "Definition" nil 0)
("awa" "auto with arith" nil 0)
("i" "intro" nil 0)
("h" "Hints :" nil 0)
("g" "generalize" nil 0)
("co" "constructor" nil 0)
("e" "elim" nil 0)
("d" "Definition" nil 0)
("c" "constructor" nil 0)
("ge" "generalize" nil 0)
("sym" "symmetry" nil 0)
("a" "auto" nil 0)
("re" "rewrite" nil 0)
("eawa" "eauto with acthint" nil 0)
("un" "unfold" nil 0)
("eaw" "eauto with" nil 0)
("fi" "functional induction" nil 0)
("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0)
("sc" "Scheme xxx := Induction for yyy Sort sss." nil 0)
("sc" "Scheme" nil 0)
("fi" "Fixpoint" nil 0)
("eap" "eapply" nil 0)
("ex" "exists" nil 0)
("inv" "inversion" nil 0)
("is" "intros" nil 0)
("abs" "absurd" nil 0)
("tr" "trivial" nil 0)
("in" "intro" nil 0)
("dis" "discriminate" nil 0)
("aw" "auto with" nil 0)
("pr" "Print" nil 0)
("au" "auto" nil 0)
("as" "assumption" nil 0)
("sy" "symmetry" nil 0)
("ar" "auto with arith" nil 0)
("el" "elim" nil 0)
("ap" "apply" nil 0)
("gen" "generalize" nil 0)
("hr" "Hint Resolve :" nil 0)
("ind" "induction" nil 0)
("fix" "Fixpoint [] : :=" nil 0)
("sp" "simpl" nil 0)
("re<" "rewrite <-" nil 0)
("ea" "eauto" nil 0)
("def" "Definition" nil 0)
))
|
