2 files changed, 8 insertions, 8 deletions
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index f0eb6a60..0940d9e7 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -18,7 +18,7 @@ method FindZero(a: array<int>) returns (r: int)
   r := -1;
 }
 
-ghost method Lemma(a: array<int>, k: int, m: int)
+lemma Lemma(a: array<int>, k: int, m: int)
   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
   requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
   requires 0 <= k;
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 41adcf50..319bb8d0 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -42,13 +42,13 @@ function ToSeq<X>(list: List<X>): seq<X>
     case Nary(nn) => ToSeq(nn) + ToSeq(rest)
 }
 
-ghost method Theorem<X>(list: List<X>)
+lemma Theorem<X>(list: List<X>)
   ensures ToSeq(list) == ToSeq(FlattenMain(list));
 {
   Lemma(list, Nil);
 }
 
-ghost method Lemma<X>(list: List<X>, ext: List<X>)
+lemma Lemma<X>(list: List<X>, ext: List<X>)
   requires IsFlat(ext);
   ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));
 {
@@ -73,27 +73,27 @@ function NegFac(n: int): int
   if -1 <= n then -1 else - NegFac(n+1) * n
 }
 
-ghost method LemmaAll()
+lemma LemmaAll()
   ensures forall n :: NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
 {
 }
 
-ghost method LemmaOne(n: int)
+lemma LemmaOne(n: int)
   ensures NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
 {
 }
 
-ghost method LemmaAll_Neg()
+lemma LemmaAll_Neg()
   ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
 
-ghost method LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int)
   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
 
-ghost method LemmaOneWithDecreases(n: int)
+lemma LemmaOneWithDecreases(n: int)
   ensures NegFac(n) <= -1;  // here, the programmer gives a good well-founded order, so this verifies
   decreases -n;
 {