diff options
| author |  Rustan Leino <unknown> | 2013-03-06 15:09:04 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-03-06 15:09:04 -0800 |
| commit | 172554c51fad4092f2b4e52a921ad0e86fa67ca6 (patch) | |
| tree | cc3c3430f1a379255f9c4990b26df1c21e06bd38 /Test/dafny3/Zip.dfy | |
| parent | d584ab2b4240b58cd4ef59e53b970a05d8d13f79 (diff) | |
Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.
Diffstat (limited to 'Test/dafny3/Zip.dfy')
| -rw-r--r-- | Test/dafny3/Zip.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy index 371b012a..80e8cd91 100644 --- a/Test/dafny3/Zip.dfy +++ b/Test/dafny3/Zip.dfy @@ -8,7 +8,7 @@ properties, drawing from: Some proofs are automatic (EvenZipLemma), whereas some others require a single
recursive call to be made explicitly.
-Note that the automatically inserted parallel statement
+Note that the automatically inserted forall statement
is in principle strong enough in all cases above, but the incompletness
of reasoning with quantifiers in SMT solvers make the explicit calls
necessary.
|