diff -r ee7413a7a44a -r 52771c21d9ca ex/NatSum.ML
--- a/ex/NatSum.ML	Wed Mar 30 10:00:23 1994 +0200
+++ b/ex/NatSum.ML	Wed Apr 06 16:31:06 1994 +0200
@@ -10,22 +10,25 @@
   ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
 
 goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
-by(nat_ind_tac "n" 1);
-by(simp_tac natsum_ss 1);
-by(asm_full_simp_tac natsum_ss 1);
+by (simp_tac natsum_ss 1);
+by (nat_ind_tac "n" 1);
+by (simp_tac natsum_ss 1);
+by (asm_simp_tac natsum_ss 1);
 result();
 
 goal NatSum.thy
   "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
 \  n*Suc(n)*Suc(Suc(Suc(0))*n)";
-by(nat_ind_tac "n" 1);
-by(simp_tac natsum_ss 1);
-by(asm_full_simp_tac natsum_ss 1);
+by (simp_tac natsum_ss 1);
+by (nat_ind_tac "n" 1);
+by (simp_tac natsum_ss 1);
+by (asm_simp_tac natsum_ss 1);
 result();
 
 goal NatSum.thy
   "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
-by(nat_ind_tac "n" 1);
-by(simp_tac natsum_ss 1);
-by(asm_full_simp_tac natsum_ss 1);
+by (simp_tac natsum_ss 1);
+by (nat_ind_tac "n" 1);
+by (simp_tac natsum_ss 1);
+by (asm_simp_tac natsum_ss 1);
 result();