From da21b5e16c55b9e8242cae9035b34a5d6c58c5af Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Wed, 5 Dec 2007 12:10:20 +0000 Subject: Corollary added to Coq starters --- coq/coq-syntax.el | 1 + 1 file changed, 1 insertion(+) (limited to 'coq/coq-syntax.el') 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 -- cgit v1.2.3