| changeset 11704 | 3c50a2cd6f00 |
| parent 11701 | 3d51fbf81c17 |
| child 15354 | 9234f5765d9c |
--- a/src/HOL/IMPP/EvenOdd.ML Fri Oct 05 23:58:52 2001 +0200 +++ b/src/HOL/IMPP/EvenOdd.ML Sat Oct 06 00:02:46 2001 +0200 @@ -17,7 +17,7 @@ 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);