src/HOL/IMPP/EvenOdd.ML

 by (Simp_tac 1);
 qed "not_even_1";
 Addsimps [not_even_1];
 
 Goalw [even_def] "even (Suc (Suc n)) = even n";
-by (subgoal_tac "Suc (Suc n) = n+# 2" 1);
+by (subgoal_tac "Suc (Suc n) = n+2" 1);
 by  (Simp_tac 2);
 by (etac ssubst 1);
 by (rtac dvd_reduce 1);
 qed "even_step";
 Addsimps[even_step];