summaryrefslogtreecommitdiff
path: root/Util/latex
diff options
context:
space:
mode:
authorGravatar boehmes <unknown>2012-09-27 17:13:42 +0200
committerGravatar boehmes <unknown>2012-09-27 17:13:42 +0200
commit623a87c132abec61b5c74a6a00a7b162073a6a8d (patch)
treeb95ba791592cf395ce99035715de98578a5519ee /Util/latex
parented83becd12d7079e6ce2853fbebace20b1e7df5a (diff)
Boogie: new syntax for integer division and modulus: use div and mod instead of / and %
Diffstat (limited to 'Util/latex')
-rw-r--r--Util/latex/boogie.sty2
1 files changed, 1 insertions, 1 deletions
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty
index 45eb050d..43336262 100644
--- a/Util/latex/boogie.sty
+++ b/Util/latex/boogie.sty
@@ -34,7 +34,7 @@
procedure,implementation,
requires,modifies,ensures,free,
% expressions
- false,true,null,old,then,
+ false,true,null,old,then,div,mod,
% statements
assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
},