3 files changed, 16 insertions, 16 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 360c5aba..fb7a5fab 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -3,10 +3,10 @@
 
 // Celebrity example, inspired by the Rodin tutorial
 
-static function method Knows<X>(a: X, b: X): bool
+function method Knows<X>(a: X, b: X): bool
   requires a != b;  // forbid asking about the reflexive case
 
-static function IsCelebrity<Y>(c: Y, people: set<Y>): bool
+function IsCelebrity<Y>(c: Y, people: set<Y>): bool
 {
   c in people &&
   (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 10b70e09..174e71c8 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -8,7 +8,7 @@ datatype Expr =
   Var(int) |
   Nary(int, List);
 
-static function Subst(e: Expr, v: int, val: int): Expr
+function Subst(e: Expr, v: int, val: int): Expr
 {
   match e
   case Const(c) => e
@@ -16,14 +16,14 @@ static function Subst(e: Expr, v: int, val: int): Expr
   case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
 }
 
-static function SubstList(l: List, v: int, val: int): List
+function SubstList(l: List, v: int, val: int): List
 {
   match l
   case Nil => l
   case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
 }
 
-static ghost method Theorem(e: Expr, v: int, val: int)
+lemma Theorem(e: Expr, v: int, val: int)
   ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
 {
   match e {
@@ -34,7 +34,7 @@ static ghost method Theorem(e: Expr, v: int, val: int)
   }
 }
 
-static ghost method Lemma(l: List, v: int, val: int)
+lemma Lemma(l: List, v: int, val: int)
   ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
 {
   match l {
@@ -52,7 +52,7 @@ datatype Expression =
   Var(int) |
   Nary(int, seq<Expression>);
 
-static function Substitute(e: Expression, v: int, val: int): Expression
+function Substitute(e: Expression, v: int, val: int): Expression
   decreases e;
 {
   match e
@@ -61,7 +61,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
   case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
 }
 
-static function SubstSeq(/*ghost*/ parent: Expression,
+function SubstSeq(/*ghost*/ parent: Expression,
                          q: seq<Expression>, v: int, val: int): seq<Expression>
   requires (forall a :: a in q ==> a < parent);
   decreases parent, q;
@@ -70,7 +70,7 @@ static function SubstSeq(/*ghost*/ parent: Expression,
   SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
 }
 
-static ghost method TheoremSeq(e: Expression, v: int, val: int)
+lemma TheoremSeq(e: Expression, v: int, val: int)
   ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
 {
   match e {
@@ -97,7 +97,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
   }
 }
 
-static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
+lemma LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
   requires (forall a :: a in q ==> a < parent);
   ensures |SubstSeq(parent, q, v, val)| == |q|;
   ensures (forall k :: 0 <= k && k < |q| ==>
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index 763cef1b..beb1597e 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -7,13 +7,13 @@ datatype List<T> = Nil | Cons(T, List<T>);
 
 datatype Tree = Node(int, List<Tree>);
 
-static function Inc(t: Tree): Tree
+function Inc(t: Tree): Tree
 {
   match t
   case Node(n, children) => Tree.Node(n+1, ForestInc(children))
 }
 
-static function ForestInc(forest: List<Tree>): List<Tree>
+function ForestInc(forest: List<Tree>): List<Tree>
 {
   match forest
   case Nil => forest
@@ -24,13 +24,13 @@ static function ForestInc(forest: List<Tree>): List<Tree>
 
 datatype GTree<T> = Node(T, List<GTree<T>>);
 
-static function GInc(t: GTree<int>): GTree<int>
+function GInc(t: GTree<int>): GTree<int>
 {
   match t
   case Node(n, children) => GTree.Node(n+1, GForestInc(children))
 }
 
-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
+function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
 {
   match forest
   case Nil => forest
@@ -43,13 +43,13 @@ datatype TreeList = Nil | Cons(OneTree, TreeList);
 
 datatype OneTree = Node(int, TreeList);
 
-static function XInc(t: OneTree): OneTree
+function XInc(t: OneTree): OneTree
 {
   match t
   case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
 }
 
-static function XForestInc(forest: TreeList): TreeList
+function XForestInc(forest: TreeList): TreeList
 {
   match forest
   case Nil => forest