Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index 46daf48d..dcc2e22d 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -225,7 +225,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
         // that FindAndStep(b) gives C[Step(u)].

         return Apply(t.car, r), value_C(t.car, C), u;

       } else {

-        parallel (C,u | IsContext(C) && t == EvalExpr(C,u))

+        forall C,u | IsContext(C) && t == EvalExpr(C,u)

           ensures Step(u) == u;

         {

           // The following assert and the first assert of each "case" are

@@ -442,7 +442,7 @@ ghost method VerificationTask3()
   ensures forall n: nat ::

     TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

 {

-  parallel (n: nat) {

+  forall n: nat {

     VT3(n);

   }

 }