From 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 Mon Sep 17 00:00:00 2001 From: Rustan Leino 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/latex/dafny.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Util/latex/dafny.sty') 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 -- cgit v1.2.3