diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-12-05 12:10:20 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-12-05 12:10:20 +0000 |
| commit | da21b5e16c55b9e8242cae9035b34a5d6c58c5af (patch) | |
| tree | 666d5ceb10fac84a0abc180515d1fb919776db6a /coq/coq-syntax.el | |
| parent | 6056026627af61aaef081bd828fb0bc8c2869a91 (diff) | |
Corollary added to Coq starters
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 88e32e30..1aa5c65d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -446,6 +446,7 @@ so for the following reasons: '( ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") ("Chapter" "chp" "Chapter # : #." t "Chapter") + ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) ("Definition" "def" "Definition #:# := #." t "Definition");; careful |