From 6a73bfff8499eb7a128de01c20488a9f53e397c7 Mon Sep 17 00:00:00 2001
From: Nadia Polikarpova <nadia.polikarpova@gmail.com>
Date: Fri, 8 Feb 2013 15:33:23 +0100
Subject: Changed calc syntax (custom operators are now written before the
 hint)

---
 Test/dafny3/CalcExample.dfy | 4 ++--
 Test/dafny3/Dijkstra.dfy    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index c94c18d2..dcd41077 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -19,8 +19,8 @@ method M(a: int, b: int, c: int, x: int)
     f(f(a, b), c);
     { assert f(a, b) == x; }
     f(x, c);
-    { assert c <= x; Monotonicity(c, x); }
-    <= f(x, x);
+    <= { assert c <= x; Monotonicity(c, x); }
+    f(x, x);
     { DiagonalIdentity(x); }
     x;
   }
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index d3ff244a..7497618c 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat)
       j <= n;
       { lemma_ping(j - 1, n - 1); }
       j - 1 <= f(n - 1);
-      { lemma_ping(j - 1, f(n - 1)); }
-      ==> j - 1 <= f(f(n - 1));
+      ==> { lemma_ping(j - 1, f(n - 1)); }
+      j - 1 <= f(f(n - 1));
       // (0)
       j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);
       ==> j - 1 < f(n);
-- 
cgit v1.2.3