summaryrefslogtreecommitdiff
path: root/Util/latex
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-11-05 01:24:43 +0000
committerGravatar rustanleino <unknown>2009-11-05 01:24:43 +0000
commitddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 (patch)
treeb2c7adc1e94b67d774aec3520d9c285662f94b60 /Util/latex
parentb5a942353fc4cf0b6a6c3df853860171e421a26a (diff)
Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)".
Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness.
Diffstat (limited to 'Util/latex')
-rw-r--r--Util/latex/dafny.sty1
1 files changed, 1 insertions, 0 deletions
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 9f7a76b3..69cd6b0a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -33,6 +33,7 @@
{<==>}{$\Longleftrightarrow$}4
{forall}{$\forall$}1
{exists}{$\exists$}1
+ {!in}{$\not\in$}1
{\\in}{$\in$}1
% the following isn't actually Dafny, but it gives the option to produce nicer latex
{<<}{$\langle$}1