1 files changed, 12 insertions, 12 deletions
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 28171896..3445dab9 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -22,7 +22,7 @@ class IntegerInduction {
 
   // Here is one proof.  It uses a lemma, which is proved separately.
 
-  ghost method Theorem0(n: int)
+  lemma Theorem0(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
   {
@@ -32,7 +32,7 @@ class IntegerInduction {
     }
   }
 
-  ghost method Lemma(n: int)
+  lemma Lemma(n: int)
     requires 0 <= n;
     ensures 2 * Gauss(n) == n*(n+1);
   {
@@ -42,7 +42,7 @@ class IntegerInduction {
   // Here is another proof.  It states the lemma as part of the theorem, and
   // thus proves the two together.
 
-  ghost method Theorem1(n: int)
+  lemma Theorem1(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
     ensures 2 * Gauss(n) == n*(n+1);
@@ -52,24 +52,24 @@ class IntegerInduction {
     }
   }
 
-  ghost method DoItAllInOneGo()
+  lemma DoItAllInOneGo()
     ensures (forall n :: 0 <= n ==>
                 SumOfCubes(n) == Gauss(n) * Gauss(n) &&
                 2 * Gauss(n) == n*(n+1));
   {
   }
 
-  // The following two ghost methods are the same as the previous two, but
+  // The following two lemmas are the same as the previous two, but
   // here no body is given--and the proof still goes through (thanks to
   // Dafny's ghost-method induction tactic).
 
-  ghost method Lemma_Auto(n: int)
+  lemma Lemma_Auto(n: int)
     requires 0 <= n;
     ensures 2 * Gauss(n) == n*(n+1);
   {
   }
 
-  ghost method Theorem1_Auto(n: int)
+  lemma Theorem1_Auto(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
     ensures 2 * Gauss(n) == n*(n+1);
@@ -79,7 +79,7 @@ class IntegerInduction {
   // Here is another proof.  It makes use of Dafny's induction heuristics to
   // prove the lemma.
 
-  ghost method Theorem2(n: int)
+  lemma Theorem2(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
   {
@@ -90,7 +90,7 @@ class IntegerInduction {
     }
   }
 
-  ghost method M(n: int)
+  lemma M(n: int)
     requires 0 <= n;
   {
     assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1));  // manually assume the induction hypothesis
@@ -99,7 +99,7 @@ class IntegerInduction {
 
   // Another way to prove the lemma is to supply a postcondition on the Gauss function
 
-  ghost method Theorem3(n: int)
+  lemma Theorem3(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
   {
@@ -117,14 +117,14 @@ class IntegerInduction {
 
   // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction
 
-  ghost method Theorem4()
+  lemma Theorem4()
     ensures (forall n :: 0 <= n ==>
         SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
   {
     // look ma, no hints!
   }
 
-  ghost method Theorem5(n: int)
+  lemma Theorem5(n: int)
     requires 0 <= n;
     ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
   {