src/ZF/ex/NatSum.ML

--- a/src/ZF/ex/NatSum.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/NatSum.ML	Mon May 21 14:36:24 2001 +0200
@@ -15,20 +15,20 @@
 Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
 
 (*The sum of the first n odd numbers equals n squared.*)
-Goal "n: nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
+Goal "n \\<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_odds";
 
 (*The sum of the first n odd squares*)
-Goal "n: nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
+Goal "n \\<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
 \     $#n $* (#4 $* $#n $* $#n $- #1)";
 by (induct_tac "n" 1);
 by Auto_tac;  
 qed "sum_of_odd_squares";
 
 (*The sum of the first n odd cubes*)
-Goal "n: nat \
+Goal "n \\<in> nat \
 \     ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
 \         $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
 by (induct_tac "n" 1);
@@ -36,18 +36,18 @@
 qed "sum_of_odd_cubes";
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "n: nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
+Goal "n \\<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_naturals";
 
-Goal "n: nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
+Goal "n \\<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
 \                $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_squares";
 
-Goal "n: nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
+Goal "n \\<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
 \                $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -55,7 +55,7 @@
 
 (** Sum of fourth powers **)
 
-Goal "n: nat ==> \
+Goal "n \\<in> nat ==> \
 \     #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
 \     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
 \     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";