From ec90ed7e102dfc76bc3677f0241494bad4c16c6f Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 24 Feb 2014 15:16:57 -0800
Subject: Minor clean-up in a couple of test files.

---
 Test/dafny1/pow2.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index c7e4bc63..bc23fb0b 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -31,20 +31,20 @@ function pow2_slow(n: int): int
     2*pow2_slow(n-1)
 }
 
-ghost method Lemma(n: int)
+lemma Lemma(n: int)
   requires 0 <= n && IsEven(n);
   ensures pow2_slow(n) == Square(pow2_slow(n/2));
 {
-  if (n != 0) {
+  if n != 0 {
     Lemma(n-2);
   }
 }
 
-ghost method Theorem(n: int)
+lemma Theorem(n: int)
   requires 0 <= n;
   ensures pow2(n) == pow2_slow(n);
 {
-  if (n == 0) {
+  if n == 0 {
   } else if (IsEven(n)) {
     Lemma(n);
     Theorem(n/2);
-- 
cgit v1.2.3