From 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 2 Aug 2013 21:44:37 -0700
Subject: Introduced keywords "lemma" (like a "ghost method", but not allowed
 to have a "modifies" clause) and "colemma" (synonymous with "comethod";
 perhaps "comethod" will go away at some point)

---
 Util/Emacs/dafny-mode.el | 2 +-
 Util/latex/dafny.sty     | 2 +-
 Util/vim/dafny.vim       | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index b043150c..c59de6ed 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -32,7 +32,7 @@
    `(,(dafny-regexp-opt '(
         "class" "datatype" "codatatype" "type" "iterator"
         "function" "predicate" "copredicate"
-        "ghost" "var" "method" "constructor" "comethod"
+        "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma"
         "abstract" "module" "import" "default" "as" "opened" "static" "refines"
         "returns" "yields" "requires" "ensures" "modifies" "reads" "free"
         "invariant" "decreases"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 6982f032..d8d4ad96 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -9,7 +9,7 @@
       bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
       function,predicate,copredicate,
       ghost,var,static,refines,
-      method,constructor,comethod,
+      method,lemma,constructor,comethod,colemma,
       returns,yields,abstract,module,import,default,opened,as,in,
       requires,modifies,ensures,reads,decreases,free,
       % expressions
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index 31f27c51..414b5fdc 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -6,7 +6,7 @@
 syntax clear
 syntax case match
 syntax keyword dafnyFunction function predicate copredicate
-syntax keyword method constructor comethod
+syntax keyword method lemma constructor comethod colemma
 syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword abstract module import opened as default
 syntax keyword dafnyConditional if then else match case 
-- 
cgit v1.2.3