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/Tree.dfy b/Test/vstte2012/Tree.dfy
index 47ed19a4..1aa06408 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -116,7 +116,7 @@ ghost method lemma1(t: Tree, s:seq<int>)
 ghost method lemma2(s: seq<int>)

   ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

 {

-  parallel(t | toList(0,t) == s) {

+  forall t | toList(0,t) == s {

     lemma1(t, s);

   } 

 }

@@ -130,7 +130,7 @@ ghost method lemma2(s: seq<int>)
 ghost method completeness()

   ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

 {

-  parallel(s) {

+  forall s {

     lemma2(s);

   }

 }