diff options
Diffstat (limited to 'Test/dafny3/Paulson.dfy')
| -rw-r--r-- | Test/dafny3/Paulson.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy index c1721af3..431ff543 100644 --- a/Test/dafny3/Paulson.dfy +++ b/Test/dafny3/Paulson.dfy @@ -150,7 +150,7 @@ ghost method Example7<A>(f: FunctionHandle<LList<A>>) // Given the definition of h, prove h(f, _) == Iterates(f, _):
ensures forall M :: h(f, M) == Iterates(f, M);
{
- forall (M) {
+ forall M {
BisimulationLemma(0, f, M);
}
}
|