1 files changed, 7 insertions, 3 deletions
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index f334e770..f88c3b54 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,9 +7,9 @@
 \lstdefinelanguage{dafny}{
   morekeywords={class,datatype,bool,int,object,set,seq,%
       function,returns,
-      var,
+      ghost,var,
       method,in,
-      requires,modifies,ensures,reads,free,
+      requires,modifies,ensures,reads,decreases,free,
       % expressions
       match,case,false,true,null,old,fresh,this,
       % statements
@@ -20,15 +20,18 @@
     {::}{$\bullet$}2
     {:=}{$:$$=$}2
     {!}{$\lnot$}1
-    {!!}{$\nparallel$}1
+    {!!}{$\not\cap$}1
     {==}{$=$}1
     {!=}{$\neq$}1
     {&&}{$\land$}1
     {||}{$\lor$}1
     {<=}{$\le$}1
     {=>}{$\ge$}1
+    % the following isn't actually Dafny, but it gives the option to produce nicer latex
+    {|=>}{$\Rightarrow$}2
     {<=set}{$\subseteq$}1
     {+set}{$\cup$}1
+    {*set}{$\cap$}1
     {==>}{$\Longrightarrow$}3 
     {<==>}{$\Longleftrightarrow$}4 
     {forall}{$\forall$}1
@@ -38,6 +41,7 @@
     % the following isn't actually Dafny, but it gives the option to produce nicer latex
     {<<}{$\langle$}1
     {>>}{$\rangle$}1
+    {...}{$\ldots$}1
     {\\alpha}{$\alpha$}1
     {\\beta}{$\beta$}1
     {\\gamma}{$\gamma$}1