diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-07-21 13:47:30 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-07-21 13:47:30 -0700 |
| commit | 7347a638cc1b1c4b573e09516edc266c91cc5620 (patch) | |
| tree | 8a57dbd6787d6b00a0b79aea6c25f530c641fbcf /Test/dafny1/Rippling.dfy | |
| parent | 2a2e483cb57d923dea66edf67093319926904a6c (diff) | |
Dafny: call previous lemma instead of restating it
Diffstat (limited to 'Test/dafny1/Rippling.dfy')
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 39e14ea5..0a4d541d 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -515,8 +515,8 @@ ghost method P46() ghost method P47()
ensures (forall a :: height(mirror(a)) == height(a));
{
- // proving this theorem requires an additional lemma:
- assert (forall x,y :: max(x,y) == max(y,x));
+ // proving this theorem requires a previously proved lemma:
+ P23();
}
// ...
|