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

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 5331b808..700b531c 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -22,7 +22,7 @@ ghost method FibLemma(n: nat)
 }

 

 /*

-  The 'parallel' statement has the effect of applying its body simultaneously

+  The 'forall' statement has the effect of applying its body simultaneously

   to all values of the bound variables---in the first example, to all k

   satisfying 0 <= k < n, and in the second example, to all non-negative n. 

 */

@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat)
 ghost method FibLemma_Alternative(n: nat)

   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

 {

-  parallel (k | 0 <= k < n) {

+  forall k | 0 <= k < n {

     FibLemma_Alternative(k);

   }

 }

@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat)
 ghost method FibLemma_All()

   ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);

 {

-  parallel (n | 0 <= n) {

+  forall n | 0 <= n {

     FibLemma(n);

   }

 }